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  48  pm2.43d  49  pm2.43a  50  imim2  54  imim1i  59  imim1  75  pm2.04  81  pm2.86  99  biimprd  156  biimpcd  157  biimprcd  158  biid  169  bibi2i  225  imbi1  234  imbi2  235  bibi1  238  pm3.3  257  pm3.31  258  jctl  307  jctr  308  ancli  316  ancri  317  anc2li  322  anc2ri  323  anim12i  331  anim1i  333  anim2i  334  pm4.24  387  anass  393  mpdan  412  mpancom  413  pm5.32  441  anbi1  454  anbi2  455  mpan10  458  simpll  496  simplr  497  simprl  498  simprr  499  pm3.45  562  pm5.36  575  con2i  590  notnot  592  con3i  595  biijust  603  con3  604  con2  605  notbii  627  pm5.19  655  olc  665  orc  666  pm2.621  699  pm1.2  706  orim1i  710  orim2i  711  pm2.41  726  pm2.42  727  pm2.4  728  pm4.44  729  orim2  736  orbi1  739  pm2.38  750  pm2.74  754  pm3.2ni  760  pm4.79dc  845  biantr  896  3anim1i  1127  3anim2i  1128  3anim3i  1129  mpd3an23  1273  trujust  1289  tru  1291  dftru2  1295  truimtru  1343  falimfal  1346  3impexp  1369  19.26  1413  19.8a  1525  19.9ht  1575  ax6blem  1583  19.36i  1605  19.41h  1618  equsb1  1712  sbieh  1717  dveeq2or  1741  spsbim  1768  2ax17  1803  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  moanmo  2022  nfcvf  2246  neqne  2259  neneq  2273  necon3i  2299  nebidc  2331  vtoclgft  2663  eueq2dc  2779  cdeqcv  2823  ru  2828  sbcied2  2865  sbcralt  2904  sbcrext  2905  csbiebt  2956  csbied2  2964  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  ssid  3033  difss2  3117  ddifstab  3121  abvor0dc  3295  ssdifeq0  3352  ifbi  3397  rabsnt  3502  unisng  3655  dfnfc2  3656  a9evsep  3938  axnul  3941  intid  4027  opm  4037  opth1  4039  opth  4040  copsex4g  4050  0nelop  4051  moop2  4054  pocl  4106  swopo  4109  limeq  4180  suceq  4205  eusvnfb  4252  onintexmid  4363  nn0eln0  4408  elvvuni  4472  coss1  4561  coss2  4562  dmxpm  4626  elrnmpt1  4656  soirri  4795  relcnvtr  4918  relssdmrn  4919  cnvpom  4941  fveqeq2  5279  fvsng  5458  isose  5563  riota2f  5592  acexmidlemab  5609  0neqopab  5653  ssoprab2  5664  caovcld  5757  caovcomd  5760  caovassd  5763  caovcand  5766  caovordid  5770  caovordd  5772  caovdid  5779  caovdird  5782  caovimo  5797  grprinvlem  5798  grprinvd  5799  f1opw  5810  caofref  5835  caofinvl  5836  xpexgALT  5863  op1stg  5880  op2ndg  5881  releldm2  5914  elopabi  5924  dfmpt2  5947  smoeq  6011  tfr1onlemaccex  6069  tfrcllemaccex  6082  rdgisucinc  6106  rdg0g  6109  oacl  6177  nna0r  6195  nnmsucr  6205  ercnv  6267  swoord1  6275  swoord2  6276  eqer  6278  ider  6279  iinerm  6318  brecop  6336  en1bg  6471  fundmeng  6478  xpsneng  6492  mapen  6516  phplem3g  6526  php5  6528  php5dom  6533  findcard2d  6561  findcard2sd  6562  undifdc  6588  xpfi  6593  ordiso2  6675  mulidnq  6895  ltsonq  6904  halfnqq  6916  nqnq0pi  6944  nq02m  6971  cauappcvgprlemm  7151  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem2  7166  cauappcvgpr  7168  ltposr  7256  0idsr  7260  1idsr  7261  ax1rid  7359  ax0id  7360  axpre-ltirr  7364  mulid1  7432  1p1times  7563  cnegexlem3  7606  pncan1  7802  npcan1  7803  kcnktkm1cn  7808  apirr  8026  recexap  8064  eqneg  8141  lediv2a  8294  nn1m1nn  8378  add1p1  8601  sub1m1  8602  cnm2m1cnm3  8603  xp1d2m1eqxm1d2  8604  div4p1lem1div2  8605  nn0addcl  8644  nn0mulcl  8645  zadd2cl  8811  nn0ledivnn  9173  nltpnft  9214  ngtmnft  9215  xrrebnd  9216  xnegneg  9230  fzss1  9411  fzssp1  9415  fzshftral  9455  0elfz  9463  nn0fz0  9464  elfz0add  9465  fz0tp  9466  elfzoelz  9489  fzoval  9490  fzoss2  9514  fzossrbm1  9515  fzouzsplit  9521  elfzo1  9532  fzonn0p1  9553  fzossfzop1  9554  fzoend  9564  fzosplitsn  9575  fvinim0ffz  9583  2tnp1ge0ge0  9639  fldiv4p1lem1div2  9643  frec2uzltd  9741  frec2uzrand  9743  uzenom  9763  frecfzennn  9764  iseqeq1  9788  iseqf1olemkle  9837  iseqf1olemklt  9838  iseqf1olemqk  9847  iseqf1olemstep  9854  iseqf1olemp  9855  iseqf1oleml  9856  iseqid  9862  iseqid2  9863  iser0f  9868  ser0f  9870  m1expcl2  9897  sqoddm1div8  10024  faclbnd  10067  facubnd  10071  bcpasc  10092  hashcl  10107  omgadd  10128  reval  10200  imval  10201  crim  10209  replim  10210  rexuz3  10340  absval  10351  sqrt0  10354  resqrexlemp1rp  10356  resqrexlemfp1  10359  resqrex  10376  leabs  10424  absimle  10434  cau3  10465  dfabsmax  10567  climshft  10608  fisum  10689  negdvdsb  10737  dvdsnegb  10738  dvdsssfz1  10778  dvds1  10779  even2n  10799  oddge22np1  10806  2tp1odd  10809  ltoddhalfle  10818  m1expo  10825  m1exp1  10826  flodddiv4  10859  gcdsupex  10874  gcdsupcl  10875  ialginv  10954  ialgcvg  10955  ialgcvga  10958  ialgfx  10959  eucialgcvga  10965  lcmdvds  10986  pw2dvds  11069  oddpwdclemodd  11075  phimul  11127  evenennn  11131  bj-ex  11151  bdth  11210  bj-dcbi  11307  bj-indind  11315
  Copyright terms: Public domain W3C validator