Editing Deduction theorem (section)

== Helpful theorems ==
If one intends to convert a complicated proof using the deduction theorem to a straight-line proof not using the deduction theorem, then it would probably be useful to prove these theorems once and for all at the beginning and then use them to help with the conversion:
:<math>A \to A</math>
helps convert the hypothesis steps.
:<math>(B \to C) \to ((A \to B) \to (A \to C))</math>
helps convert modus ponens when the major premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1.
:<math>(A \to (B \to C)) \to (B \to (A \to C))</math>
helps convert modus ponens when the minor premise is not dependent on the hypothesis, replaces axiom 2 while avoiding a use of axiom 1.

These two theorems jointly can be used in lieu of axiom 2, although the converted proof would be more complicated:
:<math>(A \to B) \to ((B \to C) \to (A \to C))</math>
:<math>(A \to (A \to C)) \to (A \to C)</math>

[[Peirce's law]] is not a consequence of the deduction theorem, but it can be used with the deduction theorem to prove things that one might not otherwise be able to prove.
:<math>((A \to B) \to A) \to A</math>
It can also be used to get the second of the two theorems, which can be used in lieu of axiom 2.