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  819  dcbiit  829  pm4.79dc  893  biantr  942  3anim1i  1175  3anim2i  1176  3anim3i  1177  mpd3an23  1329  trujust  1345  tru  1347  dftru2  1351  truimtru  1399  falimfal  1402  3impexp  1425  19.26  1469  19.8a  1578  19.9ht  1629  ax6blem  1638  19.36i  1660  19.41h  1673  equsb1  1773  sbieh  1778  dveeq2or  1804  spsbim  1831  2ax17  1866  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  moanmo  2091  nfcvf  2330  neqne  2343  neneq  2357  necon3i  2383  nebidc  2415  r19.27v  2592  r19.28v  2593  vtoclgft  2775  rspcime  2836  eueq2dc  2898  cdeqcv  2944  ru  2949  sbcied2  2987  sbcralt  3026  sbcrext  3027  csbiebt  3083  csbied2  3091  cbvralcsf  3106  cbvrexcsf  3107  cbvreucsf  3108  cbvrabcsf  3109  ssid  3161  difss2  3249  ddifstab  3253  abvor0dc  3431  ssdifeq0  3490  rabsnt  3650  unisng  3805  dfnfc2  3806  a9evsep  4103  axnul  4106  intid  4201  opm  4211  opth1  4213  opth  4214  copsex4g  4224  0nelop  4225  moop2  4228  pocl  4280  swopo  4283  limeq  4354  suceq  4379  eusvnfb  4431  onintexmid  4549  nn0eln0  4596  elvvuni  4667  coss1  4758  coss2  4759  dmxpm  4823  elrnmpt1  4854  soirri  4997  relcnvtr  5122  relssdmrn  5123  cnvpom  5145  fveqeq2  5494  fvsng  5680  isose  5788  canth  5795  riota2f  5818  acexmidlemab  5835  fvoveq1  5864  0neqopab  5883  ssoprab2  5894  caovcld  5991  caovcomd  5994  caovassd  5997  caovcand  6000  caovordid  6004  caovordd  6006  caovdid  6013  caovdird  6016  caovimo  6031  grprinvlem  6032  grprinvd  6033  f1opw  6044  caofref  6070  caofinvl  6071  xpexgALT  6098  op1stg  6115  op2ndg  6116  releldm2  6150  elopabi  6160  dfmpo  6187  smoeq  6254  tfr1onlemaccex  6312  tfrcllemaccex  6325  rdgisucinc  6349  rdg0g  6352  oacl  6424  nna0r  6442  nnmsucr  6452  ercnv  6518  swoord1  6526  swoord2  6527  eqer  6529  ider  6530  iinerm  6569  brecop  6587  ixpssmapg  6690  elixpsn  6697  en1bg  6762  fundmeng  6769  xpsneng  6784  mapen  6808  phplem3g  6818  php5  6820  php5dom  6825  findcard2d  6853  findcard2sd  6854  undifdc  6885  xpfi  6891  elfir  6934  fi0  6936  ordiso2  6996  ctssdclemr  7073  nnnninfeq2  7089  nninfisol  7093  ctssexmid  7110  exmidaclem  7160  djuenun  7164  cc1  7202  cc2lem  7203  mulidnq  7326  ltsonq  7335  halfnqq  7347  nqnq0pi  7375  nq02m  7402  cauappcvgprlemm  7582  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem2  7597  cauappcvgpr  7599  ltposr  7700  0idsr  7704  1idsr  7705  mappsrprg  7741  ax1rid  7814  ax0id  7815  axpre-ltirr  7819  mulid1  7892  1p1times  8028  cnegexlem3  8071  pncan1  8271  npcan1  8272  kcnktkm1cn  8277  apirr  8499  recexap  8546  eqneg  8624  subrecap  8731  lediv2a  8786  nn1m1nn  8871  add1p1  9102  sub1m1  9103  cnm2m1cnm3  9104  xp1d2m1eqxm1d2  9105  div4p1lem1div2  9106  nn0addcl  9145  nn0mulcl  9146  zadd2cl  9316  nn0ledivnn  9699  nltpnft  9746  ngtmnft  9749  xrrebnd  9751  xnegneg  9765  xnegid  9791  xaddid1  9794  fzss1  9994  fzssp1  9998  fzshftral  10039  0elfz  10049  nn0fz0  10050  elfz0add  10051  fz0tp  10053  elfzoelz  10078  fzoval  10079  fzoss2  10103  fzossrbm1  10104  fzouzsplit  10110  elfzo1  10121  fzonn0p1  10142  fzossfzop1  10143  fzoend  10153  fzosplitsn  10164  fvinim0ffz  10172  2tnp1ge0ge0  10232  fldiv4p1lem1div2  10236  frec2uzltd  10334  frec2uzrand  10336  uzenom  10356  frecfzennn  10357  seqeq1  10379  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqk  10425  seq3f1olemstep  10432  seq3f1olemp  10433  seq3f1oleml  10434  seq3id  10439  seq3id2  10440  ser0f  10446  m1expcl2  10473  sqoddm1div8  10604  faclbnd  10650  facubnd  10654  bcpasc  10675  hashcl  10690  omgadd  10711  reval  10787  imval  10788  crim  10796  replim  10797  rexuz3  10928  absval  10939  sqrt0  10942  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrex  10964  abs00  11002  leabs  11012  absimle  11022  cau3  11053  dfabsmax  11155  climshft  11241  fsum3  11324  fsumcnv  11374  fsumiun  11414  binom  11421  bcxmaslem1  11425  isumshft  11427  arisum  11435  arisum2  11436  trireciplem  11437  trirecip  11438  geo2sum2  11452  geo2lim  11453  prodf1f  11480  prod0  11522  fprodfac  11552  ege2le3  11608  ef4p  11631  efgt1p2  11632  efgt1p  11633  sinval  11639  cosval  11640  negdvdsb  11743  dvdsnegb  11744  dvdsssfz1  11786  dvds1  11787  even2n  11807  oddge22np1  11814  2tp1odd  11817  ltoddhalfle  11826  m1expo  11833  m1exp1  11834  flodddiv4  11867  gcdsupex  11886  gcdsupcl  11887  alginv  11975  algcvg  11976  algcvga  11979  algfx  11980  eucalgcvga  11986  lcmdvds  12007  pw2dvds  12094  oddpwdclemodd  12100  phimul  12154  eulerth  12161  pc2dvds  12257  pcz  12259  pcmpt  12269  pcmptdvds  12271  fldivp1  12274  oddprmdvds  12280  pockthg  12283  pockthi  12284  1arith  12293  zgz  12299  evenennn  12322  ennnfonelemp1  12335  ennnfonelemkh  12341  ennnfonelemnn0  12351  ssnnctlemct  12375  strslfv2  12433  strslfv  12434  ressid  12451  tsettps  12636  baspartn  12648  eltg  12652  en1top  12677  isopn3  12725  resttopon  12771  lmbr2  12814  cnptopresti  12838  cndis  12841  lmfpm  12843  lmcl  12845  lmff  12849  txswaphmeolem  12920  ispsmet  12923  psmet0  12927  xmetunirn  12958  bl2in  13003  metrest  13106  cncfmptid  13183  negcncf  13188  negfcncf  13189  limccl  13228  eldvap  13251  dvexp  13275  dveflem  13287  dvef  13288  logge0b  13411  logle1b  13413  logcxp  13418  zabsle1  13500  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdirnn0  13548  bj-ex  13603  bdth  13673  bj-indind  13774