Description: Alternate proof of id22. 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
p. 17
(PDF p. 23) at http://www.appstate.edu/~hirstjl/primer/hirst.pdf.
Note that the second occurrence of in Steps 1 to 4 and the sixth in
Step 3 may simultaneously be 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 id22.
(Contributed by
NM, 30-Sep-1992.) (New usage is discouraged.)
(Proof modification is discouraged.)