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.)