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  7838  fin23lem14  7840  fin23lem21  7846  fpwwe2cbv  8129  prsref  13872  ply1opprmul  16111  axlowdimlem13  23685  bpoly3  23896  bpoly4  23897  diophin  25947  diophren  25991  rmxfval  26084  rmyfval  26085  jm2.26lem3  26189  aomclem3  26248  dih1dimatlem  30146  dihlatat  30154  islpolN  30300  hdmapfval  30647
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator