Theorem id1 60

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is a very 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. 16 (PDF p. 22) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. For a shorter version of the proof that takes advantage of previously proved theorems, see id 59.

Assertion

Ref	Expression
id1	⊢ (φ → φ)

Proof of Theorem id1

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 ⊢ (φ → (φ → φ))
2		ax-1 4	. . 3 ⊢ (φ → ((φ → φ) → φ))
3		ax-2 5	. . 3 ⊢ ((φ → ((φ → φ) → φ)) → ((φ → (φ → φ)) → (φ → φ)))
4	2, 3	ax-mp 7	. 2 ⊢ ((φ → (φ → φ)) → (φ → φ))
5	1, 4	ax-mp 7	1 ⊢ (φ → φ)

Syntax hints:   → wi 3

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain