|Description: Alternate proof of id 22. 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's A Primer for Logic and Proof
(PDF p. 23) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf.
Note that the second occurrences of 𝜑 in Steps 1 to 4 and the sixth
in Step 3 may be simultaneously replaced by any wff 𝜓, which may
ease the understanding of the proof. For a shorter version of the proof
that takes advantage of previously proved theorems, see id 22.
(Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.)
Use id 22 instead. (New usage is