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.

- Assuming the antecedent: Based on the Deduction Metatheorem.
- Case analysis:
`(`

.*p*\/*q*) /\ (*p*=>*r*) /\ (*q*=>*r*) =>*r* - Partial evaluation (if

and*P*[*z*:=*true*]

are theorems, then so is*E*[*z*:=*false*]

):*P**P*[*z*:=*p*] == (*p*/\*E*[*z*:=*true*]) /\ (~*p*/\*E*[*z*:=*false*]) - Mutual implication:
`(`

.*p*==*q*) == (*p*=>*q*) /\ (*q*=>*p*) - Proof by contradiction:

.*p*=>*false*==*p* - Proof by contrapositive:

.*p*=>*q*== ~*q*=> ~*p*