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 6 . 2  |-  ( ph  ->  ( ph  ->  ph )
)
2 ax-1 6 . 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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  40  pm2.43i  49  pm2.43d  50  pm2.43a  51  imim2  55  imim1i  60  imim1  76  pm2.04  82  pm2.86  100  biimprd  157  biimpcd  158  biimprcd  159  biid  170  bibi2i  226  imbi1  235  imbi2  236  bibi1  239  pm3.3  259  pm3.31  260  jctl  312  jctr  313  ancli  321  ancri  322  anc2li  327  anc2ri  328  anim12i  336  anim1i  338  anim2i  339  pm4.24  392  anass  398  mpdan  417  mpancom  418  pm5.32  448  anbi1  461  anbi2  462  mpan10  465  simpll  503  simplr  504  simprl  505  simprr  506  pm3.45  571  pm5.36  584  con2i  601  notnot  603  con3i  606  biijust  615  con3  616  con2  617  pm5.19  680  olc  685  orc  686  pm2.621  721  pm1.2  730  orim1i  734  orim2i  735  pm2.41  750  pm2.42  751  pm2.4  752  pm4.44  753  orim2  763  orbi1  766  pm2.38  777  pm2.74  781  pm3.2ni  787  dcbiit  809  pm4.79dc  873  biantr  921  3anim1i  1152  3anim2i  1153  3anim3i  1154  mpd3an23  1302  trujust  1318  tru  1320  dftru2  1324  truimtru  1372  falimfal  1375  3impexp  1398  19.26  1442  19.8a  1554  19.9ht  1605  ax6blem  1613  19.36i  1635  19.41h  1648  equsb1  1743  sbieh  1748  dveeq2or  1772  spsbim  1799  2ax17  1834  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  moanmo  2054  nfcvf  2280  neqne  2293  neneq  2307  necon3i  2333  nebidc  2365  r19.27v  2536  r19.28v  2537  vtoclgft  2710  rspcime  2770  eueq2dc  2830  cdeqcv  2876  ru  2881  sbcied2  2918  sbcralt  2957  sbcrext  2958  csbiebt  3009  csbied2  3017  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  ssid  3087  difss2  3174  ddifstab  3178  abvor0dc  3356  ssdifeq0  3415  rabsnt  3568  unisng  3723  dfnfc2  3724  a9evsep  4020  axnul  4023  intid  4116  opm  4126  opth1  4128  opth  4129  copsex4g  4139  0nelop  4140  moop2  4143  pocl  4195  swopo  4198  limeq  4269  suceq  4294  eusvnfb  4345  onintexmid  4457  nn0eln0  4503  elvvuni  4573  coss1  4664  coss2  4665  dmxpm  4729  elrnmpt1  4760  soirri  4903  relcnvtr  5028  relssdmrn  5029  cnvpom  5051  fveqeq2  5398  fvsng  5584  isose  5690  riota2f  5719  acexmidlemab  5736  fvoveq1  5765  0neqopab  5784  ssoprab2  5795  caovcld  5892  caovcomd  5895  caovassd  5898  caovcand  5901  caovordid  5905  caovordd  5907  caovdid  5914  caovdird  5917  caovimo  5932  grprinvlem  5933  grprinvd  5934  f1opw  5945  caofref  5971  caofinvl  5972  xpexgALT  5999  op1stg  6016  op2ndg  6017  releldm2  6051  elopabi  6061  dfmpo  6088  smoeq  6155  tfr1onlemaccex  6213  tfrcllemaccex  6226  rdgisucinc  6250  rdg0g  6253  oacl  6324  nna0r  6342  nnmsucr  6352  ercnv  6418  swoord1  6426  swoord2  6427  eqer  6429  ider  6430  iinerm  6469  brecop  6487  ixpssmapg  6590  elixpsn  6597  en1bg  6662  fundmeng  6669  xpsneng  6684  mapen  6708  phplem3g  6718  php5  6720  php5dom  6725  findcard2d  6753  findcard2sd  6754  undifdc  6780  xpfi  6786  elfir  6829  fi0  6831  ordiso2  6888  ctssdclemr  6965  ctssexmid  6992  exmidaclem  7032  djuenun  7036  mulidnq  7165  ltsonq  7174  halfnqq  7186  nqnq0pi  7214  nq02m  7241  cauappcvgprlemm  7421  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem2  7436  cauappcvgpr  7438  ltposr  7539  0idsr  7543  1idsr  7544  mappsrprg  7580  ax1rid  7653  ax0id  7654  axpre-ltirr  7658  mulid1  7731  1p1times  7864  cnegexlem3  7907  pncan1  8107  npcan1  8108  kcnktkm1cn  8113  apirr  8334  recexap  8381  eqneg  8459  lediv2a  8617  nn1m1nn  8702  add1p1  8927  sub1m1  8928  cnm2m1cnm3  8929  xp1d2m1eqxm1d2  8930  div4p1lem1div2  8931  nn0addcl  8970  nn0mulcl  8971  zadd2cl  9138  nn0ledivnn  9509  nltpnft  9552  ngtmnft  9555  xrrebnd  9557  xnegneg  9571  xnegid  9597  xaddid1  9600  fzss1  9798  fzssp1  9802  fzshftral  9843  0elfz  9853  nn0fz0  9854  elfz0add  9855  fz0tp  9856  elfzoelz  9879  fzoval  9880  fzoss2  9904  fzossrbm1  9905  fzouzsplit  9911  elfzo1  9922  fzonn0p1  9943  fzossfzop1  9944  fzoend  9954  fzosplitsn  9965  fvinim0ffz  9973  2tnp1ge0ge0  10029  fldiv4p1lem1div2  10033  frec2uzltd  10131  frec2uzrand  10133  uzenom  10153  frecfzennn  10154  seqeq1  10176  iseqf1olemkle  10212  iseqf1olemklt  10213  iseqf1olemqk  10222  seq3f1olemstep  10229  seq3f1olemp  10230  seq3f1oleml  10231  seq3id  10236  seq3id2  10237  ser0f  10243  m1expcl2  10270  sqoddm1div8  10399  faclbnd  10442  facubnd  10446  bcpasc  10467  hashcl  10482  omgadd  10503  reval  10576  imval  10577  crim  10585  replim  10586  rexuz3  10717  absval  10728  sqrt0  10731  resqrexlemp1rp  10733  resqrexlemfp1  10736  resqrex  10753  abs00  10791  leabs  10801  absimle  10811  cau3  10842  dfabsmax  10944  climshft  11028  fsum3  11111  fsumcnv  11161  fsumiun  11201  binom  11208  bcxmaslem1  11212  isumshft  11214  arisum  11222  arisum2  11223  trireciplem  11224  trirecip  11225  geo2sum2  11239  geo2lim  11240  ege2le3  11291  ef4p  11314  efgt1p2  11315  efgt1p  11316  sinval  11323  cosval  11324  negdvdsb  11421  dvdsnegb  11422  dvdsssfz1  11462  dvds1  11463  even2n  11483  oddge22np1  11490  2tp1odd  11493  ltoddhalfle  11502  m1expo  11509  m1exp1  11510  flodddiv4  11543  gcdsupex  11558  gcdsupcl  11559  alginv  11640  algcvg  11641  algcvga  11644  algfx  11645  eucalgcvga  11651  lcmdvds  11672  pw2dvds  11755  oddpwdclemodd  11761  phimul  11813  evenennn  11817  ennnfonelemp1  11830  ennnfonelemkh  11836  ennnfonelemnn0  11846  strslfv2  11913  strslfv  11914  ressid  11931  tsettps  12116  baspartn  12128  eltg  12132  en1top  12157  isopn3  12205  resttopon  12251  lmbr2  12294  cnptopresti  12318  cndis  12321  lmfpm  12323  lmcl  12325  lmff  12329  txswaphmeolem  12400  ispsmet  12403  psmet0  12407  xmetunirn  12438  bl2in  12483  metrest  12586  cncfmptid  12663  negcncf  12668  negfcncf  12669  limccl  12708  eldvap  12731  dvexp  12755  dveflem  12766  dvef  12767  bj-ex  12865  bdth  12925  bj-indind  13026
  Copyright terms: Public domain W3C validator