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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- ( ph -> ( ph -> ph ) )
2		ax-1 6	. 2 |- ( ph -> ( ( ph -> ph ) -> ph ) )
3	1, 2	mpd 13	1 |- ( ph -> ph )

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  anim1ci  339  anim2i  340  pm4.24  393  anass  399  mpdan  418  mpancom  419  pm5.32  449  anbi1  462  anbi2  463  mpan10  466  adantl3r  504  simpll  519  simplr  520  simprl  521  simprr  522  pm3.45  587  pm5.36  600  con2i  617  notnot  619  con3i  622  biijust  631  con3  632  con2  633  pm5.19  696  olc  701  orc  702  pm2.621  737  pm1.2  746  orim1i  750  orim2i  751  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  orim2  779  orbi1  782  pm2.38  793  pm2.74  797  pm3.2ni  803  biort  815  dcbiit  825  pm4.79dc  889  biantr  937  3anim1i  1168  3anim2i  1169  3anim3i  1170  mpd3an23  1321  trujust  1337  tru  1339  dftru2  1343  truimtru  1391  falimfal  1394  3impexp  1417  19.26  1461  19.8a  1570  19.9ht  1621  ax6blem  1630  19.36i  1652  19.41h  1665  equsb1  1765  sbieh  1770  dveeq2or  1796  spsbim  1823  2ax17  1858  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  moanmo  2083  nfcvf  2322  neqne  2335  neneq  2349  necon3i  2375  nebidc  2407  r19.27v  2584  r19.28v  2585  vtoclgft  2762  rspcime  2823  eueq2dc  2885  cdeqcv  2931  ru  2936  sbcied2  2974  sbcralt  3013  sbcrext  3014  csbiebt  3070  csbied2  3078  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  ssid  3148  difss2  3236  ddifstab  3240  abvor0dc  3418  ssdifeq0  3477  rabsnt  3636  unisng  3791  dfnfc2  3792  a9evsep  4089  axnul  4092  intid  4187  opm  4197  opth1  4199  opth  4200  copsex4g  4210  0nelop  4211  moop2  4214  pocl  4266  swopo  4269  limeq  4340  suceq  4365  eusvnfb  4417  onintexmid  4535  nn0eln0  4582  elvvuni  4653  coss1  4744  coss2  4745  dmxpm  4809  elrnmpt1  4840  soirri  4983  relcnvtr  5108  relssdmrn  5109  cnvpom  5131  fveqeq2  5480  fvsng  5666  isose  5774  canth  5781  riota2f  5804  acexmidlemab  5821  fvoveq1  5850  0neqopab  5869  ssoprab2  5880  caovcld  5977  caovcomd  5980  caovassd  5983  caovcand  5986  caovordid  5990  caovordd  5992  caovdid  5999  caovdird  6002  caovimo  6017  grprinvlem  6018  grprinvd  6019  f1opw  6030  caofref  6056  caofinvl  6057  xpexgALT  6084  op1stg  6101  op2ndg  6102  releldm2  6136  elopabi  6146  dfmpo  6173  smoeq  6240  tfr1onlemaccex  6298  tfrcllemaccex  6311  rdgisucinc  6335  rdg0g  6338  oacl  6410  nna0r  6428  nnmsucr  6438  ercnv  6504  swoord1  6512  swoord2  6513  eqer  6515  ider  6516  iinerm  6555  brecop  6573  ixpssmapg  6676  elixpsn  6683  en1bg  6748  fundmeng  6755  xpsneng  6770  mapen  6794  phplem3g  6804  php5  6806  php5dom  6811  findcard2d  6839  findcard2sd  6840  undifdc  6871  xpfi  6877  elfir  6920  fi0  6922  ordiso2  6982  ctssdclemr  7059  nnnninfeq2  7075  nninfisol  7079  ctssexmid  7096  exmidaclem  7146  djuenun  7150  cc1  7188  cc2lem  7189  mulidnq  7312  ltsonq  7321  halfnqq  7333  nqnq0pi  7361  nq02m  7388  cauappcvgprlemm  7568  cauappcvgprlemloc  7575  cauappcvgprlemladdru  7579  cauappcvgprlemladdrl  7580  cauappcvgprlem2  7583  cauappcvgpr  7585  ltposr  7686  0idsr  7690  1idsr  7691  mappsrprg  7727  ax1rid  7800  ax0id  7801  axpre-ltirr  7805  mulid1  7878  1p1times  8014  cnegexlem3  8057  pncan1  8257  npcan1  8258  kcnktkm1cn  8263  apirr  8485  recexap  8532  eqneg  8610  subrecap  8717  lediv2a  8772  nn1m1nn  8857  add1p1  9088  sub1m1  9089  cnm2m1cnm3  9090  xp1d2m1eqxm1d2  9091  div4p1lem1div2  9092  nn0addcl  9131  nn0mulcl  9132  zadd2cl  9299  nn0ledivnn  9681  nltpnft  9725  ngtmnft  9728  xrrebnd  9730  xnegneg  9744  xnegid  9770  xaddid1  9773  fzss1  9972  fzssp1  9976  fzshftral  10017  0elfz  10027  nn0fz0  10028  elfz0add  10029  fz0tp  10031  elfzoelz  10056  fzoval  10057  fzoss2  10081  fzossrbm1  10082  fzouzsplit  10088  elfzo1  10099  fzonn0p1  10120  fzossfzop1  10121  fzoend  10131  fzosplitsn  10142  fvinim0ffz  10150  2tnp1ge0ge0  10210  fldiv4p1lem1div2  10214  frec2uzltd  10312  frec2uzrand  10314  uzenom  10334  frecfzennn  10335  seqeq1  10357  iseqf1olemkle  10393  iseqf1olemklt  10394  iseqf1olemqk  10403  seq3f1olemstep  10410  seq3f1olemp  10411  seq3f1oleml  10412  seq3id  10417  seq3id2  10418  ser0f  10424  m1expcl2  10451  sqoddm1div8  10581  faclbnd  10627  facubnd  10631  bcpasc  10652  hashcl  10667  omgadd  10688  reval  10761  imval  10762  crim  10770  replim  10771  rexuz3  10902  absval  10913  sqrt0  10916  resqrexlemp1rp  10918  resqrexlemfp1  10921  resqrex  10938  abs00  10976  leabs  10986  absimle  10996  cau3  11027  dfabsmax  11129  climshft  11213  fsum3  11296  fsumcnv  11346  fsumiun  11386  binom  11393  bcxmaslem1  11397  isumshft  11399  arisum  11407  arisum2  11408  trireciplem  11409  trirecip  11410  geo2sum2  11424  geo2lim  11425  prodf1f  11452  prod0  11494  fprodfac  11524  ege2le3  11580  ef4p  11603  efgt1p2  11604  efgt1p  11605  sinval  11611  cosval  11612  negdvdsb  11715  dvdsnegb  11716  dvdsssfz1  11757  dvds1  11758  even2n  11778  oddge22np1  11785  2tp1odd  11788  ltoddhalfle  11797  m1expo  11804  m1exp1  11805  flodddiv4  11838  gcdsupex  11857  gcdsupcl  11858  alginv  11940  algcvg  11941  algcvga  11944  algfx  11945  eucalgcvga  11951  lcmdvds  11972  pw2dvds  12057  oddpwdclemodd  12063  phimul  12117  eulerth  12124  evenennn  12218  ennnfonelemp1  12231  ennnfonelemkh  12237  ennnfonelemnn0  12247  ssnnctlemct  12271  strslfv2  12329  strslfv  12330  ressid  12347  tsettps  12532  baspartn  12544  eltg  12548  en1top  12573  isopn3  12621  resttopon  12667  lmbr2  12710  cnptopresti  12734  cndis  12737  lmfpm  12739  lmcl  12741  lmff  12745  txswaphmeolem  12816  ispsmet  12819  psmet0  12823  xmetunirn  12854  bl2in  12899  metrest  13002  cncfmptid  13079  negcncf  13084  negfcncf  13085  limccl  13124  eldvap  13147  dvexp  13171  dveflem  13183  dvef  13184  logge0b  13307  logle1b  13309  logcxp  13314  bj-ex  13433  bdth  13503  bj-indind  13604