One of the objects of our rigorous approach to proof is to explain how informal proof methods are grounded in logic. In Chapter 4 of A Logical Approach to Discrete Math, we explain how each informal technique has a solid foundation underneath it, in the form of a theorem or metatheorem. Here is a list of informal techniques together with the theorems on which they are based.
(p \/ q) /\ (p => r) /\ (q => r) => r.
E[z:= false]are theorems, then so is
P[z:= p] == (p /\ E[z:= true]) /\ (~p /\ E[z:= false])
(p == q) == (p => q) /\ (q => p).
p => false == p.
p => q == ~q => ~p.