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  7911  fin23lem14  7913  fin23lem21  7919  fpwwe2cbv  8206  prsref  14014  ply1opprmul  16265  axlowdimlem13  23943  bpoly3  24154  bpoly4  24155  diophin  26205  diophren  26249  rmxfval  26342  rmyfval  26343  jm2.26lem3  26447  aomclem3  26506  dih1dimatlem  30670  dihlatat  30678  islpolN  30824  hdmapfval  31171
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator