**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*
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 id 22.
(Contributed by
NM, 30-Sep-1992.) (Proof modification is discouraged.) Use id 22
instead. (New usage is discouraged.) |