ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  id Unicode version

Theorem id 19
Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Assertion
Ref Expression
id  |-  ( ph  ->  ph )

Proof of Theorem id
StepHypRef Expression
1 ax-1 5 . 2  |-  ( ph  ->  ( ph  ->  ph )
)
2 ax-1 5 . 2  |-  ( ph  ->  ( ( ph  ->  ph )  ->  ph ) )
31, 2mpd 13 1  |-  ( ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  39  pm2.43i  47  pm2.43d  48  pm2.43a  49  imim2  53  imim1i  58  imim1  74  pm2.04  80  pm2.86  98  biimprd  151  biimpcd  152  biimprcd  153  biid  164  bibi2i  220  imbi1  229  imbi2  230  bibi1  233  pm3.3  252  pm3.31  253  jctl  301  jctr  302  ancli  310  ancri  311  anc2li  316  anc2ri  317  anim12i  325  anim1i  327  anim2i  328  pm4.24  381  anass  387  mpdan  406  mpancom  407  pm5.32  434  anbi1  447  anbi2  448  mpan10  451  simpll  489  simplr  490  simprl  491  simprr  492  pm3.45  539  pm5.36  552  con2i  567  notnot  569  con3i  572  biijust  580  con3  581  con2  582  notbii  604  pm5.19  632  olc  642  orc  643  pm2.621  676  pm1.2  683  orim1i  687  orim2i  688  pm2.41  703  pm2.42  704  pm2.4  705  pm4.44  706  orim2  713  orbi1  716  pm2.38  727  pm2.74  731  pm3.2ni  737  pm4.79dc  820  biantr  870  3anim1i  1101  3anim2i  1102  3anim3i  1103  mpd3an23  1245  trujust  1261  tru  1263  dftru2  1267  truimtru  1316  falimfal  1319  3impexp  1342  19.26  1386  19.8a  1498  19.9ht  1548  ax6blem  1556  19.36i  1578  19.41h  1591  equsb1  1684  sbieh  1689  dveeq2or  1713  spsbim  1740  2ax17  1774  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  moanmo  1993  nfcvf  2215  neqne  2228  neneq  2242  necon3i  2268  nebidc  2300  vtoclgft  2621  eueq2dc  2737  cdeqcv  2781  ru  2786  sbcied2  2823  sbcralt  2862  sbcrext  2863  csbiebt  2914  csbied2  2921  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  ssid  2992  sspsstr  3078  psssstr  3079  difss2  3100  abvor0dc  3270  ssdifeq0  3333  ifbi  3376  rabsnt  3473  unisng  3625  dfnfc2  3626  a9evsep  3907  axnul  3910  intid  3988  opm  3999  opth1  4001  opth  4002  copsex4g  4012  0nelop  4013  moop2  4016  pocl  4068  swopo  4071  limeq  4142  suceq  4167  eusvnfb  4214  onintexmid  4325  nn0eln0  4369  elvvuni  4432  coss1  4519  coss2  4520  dmxpm  4583  elrnmpt1  4613  soirri  4747  relcnvtr  4868  relssdmrn  4869  cnvpom  4888  fvsng  5387  isose  5488  riota2f  5517  acexmidlemab  5534  0neqopab  5578  ssoprab2  5589  caovcld  5682  caovcomd  5685  caovassd  5688  caovcand  5691  caovordid  5695  caovordd  5697  caovdid  5704  caovdird  5707  caovimo  5722  grprinvlem  5723  grprinvd  5724  f1opw  5735  caofref  5760  caofinvl  5761  xpexgALT  5788  op1stg  5805  op2ndg  5806  releldm2  5839  elopabi  5849  dfmpt2  5872  smoeq  5936  rdgisucinc  6003  rdg0g  6006  oacl  6071  nna0r  6088  nnmsucr  6098  ercnv  6158  swoord1  6166  swoord2  6167  eqer  6169  ider  6170  iinerm  6209  brecop  6227  en1bg  6311  fundmeng  6318  xpsneng  6327  phplem3g  6350  php5  6352  php5dom  6356  findcard2d  6379  findcard2sd  6380  ordiso2  6415  mulidnq  6545  ltsonq  6554  halfnqq  6566  nqnq0pi  6594  nq02m  6621  cauappcvgprlemm  6801  cauappcvgprlemloc  6808  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem2  6816  cauappcvgpr  6818  ltposr  6906  0idsr  6910  1idsr  6911  ax1rid  7009  ax0id  7010  axpre-ltirr  7014  mulid1  7082  1p1times  7208  cnegexlem3  7251  pncan1  7447  npcan1  7448  kcnktkm1cn  7452  apirr  7670  recexap  7708  eqneg  7783  lediv2a  7936  nn1m1nn  8008  add1p1  8231  sub1m1  8232  cnm2m1cnm3  8233  xp1d2m1eqxm1d2  8234  div4p1lem1div2  8235  nn0addcl  8274  nn0mulcl  8275  zadd2cl  8426  nn0ledivnn  8785  nltpnft  8831  ngtmnft  8832  xrrebnd  8833  xnegneg  8847  fzss1  9028  fzssp1  9032  fzshftral  9072  0elfz  9079  nn0fz0  9080  elfz0add  9081  fz0tp  9083  elfzoelz  9106  fzoval  9107  fzoss2  9130  fzossrbm1  9131  fzouzsplit  9137  elfzo1  9148  fzonn0p1  9169  fzossfzop1  9170  fzoend  9180  fzosplitsn  9191  fvinim0ffz  9198  2tnp1ge0ge0  9251  fldiv4p1lem1div2  9255  frec2uzltd  9353  frec2uzrand  9355  uzenom  9366  frecfzennn  9367  iseqeq1  9378  iseqid  9411  iser0f  9416  m1expcl2  9442  sqoddm1div8  9569  faclbnd  9609  facubnd  9613  bcpasc  9634  reval  9677  imval  9678  crim  9686  replim  9687  rexuz3  9817  absval  9828  sqrt0  9831  resqrexlemp1rp  9833  resqrexlemfp1  9836  resqrex  9853  leabs  9901  absimle  9911  cau3  9942  climshft  10056  negdvdsb  10124  dvdsnegb  10125  dvdsssfz1  10164  dvds1  10165  even2n  10185  oddge22np1  10193  2tp1odd  10196  ltoddhalfle  10205  m1expo  10212  m1exp1  10213  flodddiv4  10246  pw2dvds  10254  oddpwdclemodd  10260  ialginv  10269  ialgcvg  10270  ialgcvga  10273  ialgfx  10274  bj-ex  10289  bdth  10338  bj-dcbi  10435  bj-indind  10443
  Copyright terms: Public domain W3C validator