Theorem idALT

Description: Alternate proof of id . This version is proved directly from the axioms for demonstration purposes. This proof is a popular example in the literature and is identical, step for step, to the proofs of Theorem 1 of Margaris p. 51, Example 2.7(a) of Hamilton p. 31, Lemma 10.3 of BellMachover p. 36, and Lemma 1.8 of Mendelson p. 36. It is also "Our first proof" in Hirst and Hirst'sA Primer for Logic and Proof p. 17 (PDF p. 23) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf . Note that the second occurrences of ph in Steps 1 to 4 and the sixth in Step 3 may be simultaneously replaced by any wff ps , which may ease the understanding of the proof. For a shorter version of the proof that takes advantage of previously proved theorems, see id . (Contributed by NM, 30-Sep-1992) (Proof modification is discouraged.) Use id instead. (New usage is discouraged.)

	Ref	Expression
Assertion	idALT	$$⊢\phi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢\phi \to \left(\phi \to \phi \right)$$
2		ax-1	$$⊢\phi \to \left(\left(\phi \to \phi \right)\to \phi \right)$$
3		ax-2	$$⊢\left(\phi \to \left(\left(\phi \to \phi \right)\to \phi \right)\right)\to \left(\left(\phi \to \left(\phi \to \phi \right)\right)\to \left(\phi \to \phi \right)\right)$$
4	2 3	ax-mp	$$⊢\left(\phi \to \left(\phi \to \phi \right)\right)\to \left(\phi \to \phi \right)$$
5	1 4	ax-mp	$$⊢\phi \to \phi$$