Theorem id1 10

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 identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51 and Example 2.7(a) of [Hamilton] p. 31. For a shorter version of the proof that takes advantage of a previously proved inference, see id 9.

Assertion

Ref	Expression
id1	⊢ (φ → φ)

Proof of Theorem id1

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

Syntax hints:   → wi 2

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org