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	|- (ph -> ph)

Proof of Theorem id1

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 |- (ph -> (ph -> ph))
2		ax-1 3	. . 3 |- (ph -> ((ph -> ph) -> ph))
3		ax-2 4	. . 3 |- ((ph -> ((ph -> ph) -> ph)) -> ((ph -> (ph -> ph)) -> (ph -> ph)))
4	2, 3	ax-mp 6	. 2 |- ((ph -> (ph -> ph)) -> (ph -> ph))
5	1, 4	ax-mp 6	1 |- (ph -> ph)

Syntax hints:   -> wi 2

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

metamath.org