MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  id1 Unicode version

Theorem id1 22
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 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.mathsci.appstate.edu/~jlh/primer/hirst.pdf. For a shorter version of the proof that takes advantage of previously proved theorems, see id 21. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.)
Assertion
Ref Expression
id1  |-  ( ph  ->  ph )

Proof of Theorem id1
StepHypRef Expression
1 ax-1 7 . 2  |-  ( ph  ->  ( ph  ->  ph )
)
2 ax-1 7 . . 3  |-  ( ph  ->  ( ( ph  ->  ph )  ->  ph ) )
3 ax-2 8 . . 3  |-  ( (
ph  ->  ( ( ph  ->  ph )  ->  ph )
)  ->  ( ( ph  ->  ( ph  ->  ph ) )  ->  ( ph  ->  ph ) ) )
42, 3ax-mp 10 . 2  |-  ( (
ph  ->  ( ph  ->  ph ) )  ->  ( ph  ->  ph ) )
51, 4ax-mp 10 1  |-  ( ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  fin23lem12  7841  fin23lem14  7843  fin23lem21  7849  fpwwe2cbv  8132  prsref  13910  ply1opprmul  16149  axlowdimlem13  23756  bpoly3  23967  bpoly4  23968  diophin  26018  diophren  26062  rmxfval  26155  rmyfval  26156  jm2.26lem3  26260  aomclem3  26319  dih1dimatlem  30208  dihlatat  30216  islpolN  30362  hdmapfval  30709
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator