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  101  biimprd  158  biimpcd  159  biimprcd  160  biid  171  bibi2i  227  imbi1  236  imbi2  237  bibi1  240  pm3.3  261  pm3.31  262  jctl  314  jctr  315  ancli  323  ancri  324  anc2li  329  anc2ri  330  anim12i  338  anim1i  340  anim1ci  341  anim2i  342  pm4.24  395  anass  401  mpdan  421  mpancom  422  pm5.32  453  anbi1  466  anbi2  467  mpan10  474  adantl3r  512  simpll  527  simplr  528  simprl  529  simprr  531  pm3.45  597  pm5.36  610  con2i  628  notnot  630  con3i  633  biijust  642  con3  643  con2  644  pm5.19  707  olc  712  orc  713  pm2.621  748  pm1.2  757  orim1i  761  orim2i  762  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  orim2  790  orbi1  793  pm2.38  804  pm2.74  808  pm3.2ni  814  biort  830  dcbiit  840  pm4.79dc  904  biantr  953  3anim1i  1186  3anim2i  1187  3anim3i  1188  mpd3an23  1349  trujust  1365  tru  1367  dftru2  1371  truimtru  1419  falimfal  1422  3impexp  1447  19.26  1491  19.8a  1600  19.9ht  1651  ax6blem  1660  19.36i  1682  19.41h  1695  equsb1  1795  sbieh  1800  dveeq2or  1826  spsbim  1853  2ax17  1888  dvelimALT  2020  dvelimfv  2021  dvelimor  2028  moanmo  2113  nfcvf  2352  neqne  2365  neneq  2379  necon3i  2405  nebidc  2437  r19.27v  2614  r19.28v  2615  vtoclgft  2799  rspcime  2860  eueq2dc  2922  cdeqcv  2968  ru  2973  sbcied2  3012  sbcralt  3051  sbcrext  3052  csbiebt  3108  csbied2  3116  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  ssid  3187  difss2  3275  ddifstab  3279  abvor0dc  3458  ssdifeq0  3517  rabsnt  3679  unisng  3838  dfnfc2  3839  a9evsep  4137  axnul  4140  intid  4236  opm  4246  opth1  4248  opth  4249  copsex4g  4259  0nelop  4260  moop2  4263  pocl  4315  swopo  4318  limeq  4389  suceq  4414  eusvnfb  4466  onintexmid  4584  nn0eln0  4631  elvvuni  4702  coss1  4794  coss2  4795  dmxpm  4859  elrnmpt1  4890  soirri  5035  relcnvtr  5160  relssdmrn  5161  cnvpom  5183  fveqeq2  5536  fvsng  5725  isose  5835  canth  5842  riota2f  5865  acexmidlemab  5882  fvoveq1  5911  0neqopab  5933  ssoprab2  5944  caovcld  6041  caovcomd  6044  caovassd  6047  caovcand  6050  caovordid  6054  caovordd  6056  caovdid  6063  caovdird  6066  caovimo  6081  f1opw  6091  caofref  6117  caofinvl  6118  xpexgALT  6147  op1stg  6164  op2ndg  6165  releldm2  6199  elopabi  6209  dfmpo  6237  smoeq  6304  tfr1onlemaccex  6362  tfrcllemaccex  6375  rdgisucinc  6399  rdg0g  6402  oacl  6474  nna0r  6492  nnmsucr  6502  ercnv  6569  swoord1  6577  swoord2  6578  eqer  6580  ider  6581  iinerm  6620  brecop  6638  ixpssmapg  6741  elixpsn  6748  en1bg  6813  fundmeng  6820  xpsneng  6835  mapen  6859  phplem3g  6869  php5  6871  php5dom  6876  findcard2d  6904  findcard2sd  6905  undifdc  6936  xpfi  6942  elfir  6985  fi0  6987  ordiso2  7047  ctssdclemr  7124  nnnninfeq2  7140  nninfisol  7144  ctssexmid  7161  exmidaclem  7220  djuenun  7224  exmidapne  7272  cc1  7277  cc2lem  7278  mulidnq  7401  ltsonq  7410  halfnqq  7422  nqnq0pi  7450  nq02m  7477  cauappcvgprlemm  7657  cauappcvgprlemloc  7664  cauappcvgprlemladdru  7668  cauappcvgprlemladdrl  7669  cauappcvgprlem2  7672  cauappcvgpr  7674  ltposr  7775  0idsr  7779  1idsr  7780  mappsrprg  7816  ax1rid  7889  ax0id  7890  axpre-ltirr  7894  mulrid  7967  1p1times  8104  cnegexlem3  8147  pncan1  8347  npcan1  8348  kcnktkm1cn  8353  apirr  8575  recexap  8623  eqneg  8702  subrecap  8809  lediv2a  8865  nn1m1nn  8950  add1p1  9181  sub1m1  9182  cnm2m1cnm3  9183  xp1d2m1eqxm1d2  9184  div4p1lem1div2  9185  nn0addcl  9224  nn0mulcl  9225  zadd2cl  9395  nn0ledivnn  9780  nltpnft  9827  ngtmnft  9830  xrrebnd  9832  xnegneg  9846  xnegid  9872  xaddid1  9875  fzss1  10076  fzssp1  10080  fzshftral  10121  0elfz  10131  nn0fz0  10132  elfz0add  10133  fz0tp  10135  elfzoelz  10160  fzoval  10161  fzoss2  10185  fzossrbm1  10186  fzouzsplit  10192  elfzo1  10203  fzonn0p1  10224  fzossfzop1  10225  fzoend  10235  fzosplitsn  10246  fvinim0ffz  10254  2tnp1ge0ge0  10314  fldiv4p1lem1div2  10318  frec2uzltd  10416  frec2uzrand  10418  uzenom  10438  frecfzennn  10439  seqeq1  10461  iseqf1olemkle  10497  iseqf1olemklt  10498  iseqf1olemqk  10507  seq3f1olemstep  10514  seq3f1olemp  10515  seq3f1oleml  10516  seq3id  10521  seq3id2  10522  ser0f  10528  m1expcl2  10555  sqoddm1div8  10687  mulsubdivbinom2ap  10704  faclbnd  10734  facubnd  10738  bcpasc  10759  hashcl  10774  omgadd  10795  reval  10871  imval  10872  crim  10880  replim  10881  rexuz3  11012  absval  11023  sqrt0  11026  resqrexlemp1rp  11028  resqrexlemfp1  11031  resqrex  11048  abs00  11086  leabs  11096  absimle  11106  cau3  11137  dfabsmax  11239  climshft  11325  fsum3  11408  fsumcnv  11458  fsumiun  11498  binom  11505  bcxmaslem1  11509  isumshft  11511  arisum  11519  arisum2  11520  trireciplem  11521  trirecip  11522  geo2sum2  11536  geo2lim  11537  prodf1f  11564  prod0  11606  fprodfac  11636  ege2le3  11692  ef4p  11715  efgt1p2  11716  efgt1p  11717  sinval  11723  cosval  11724  negdvdsb  11827  dvdsnegb  11828  dvdsssfz1  11871  dvds1  11872  even2n  11892  oddge22np1  11899  2tp1odd  11902  ltoddhalfle  11911  m1expo  11918  m1exp1  11919  flodddiv4  11952  gcdsupex  11971  gcdsupcl  11972  alginv  12060  algcvg  12061  algcvga  12064  algfx  12065  eucalgcvga  12071  lcmdvds  12092  pw2dvds  12179  oddpwdclemodd  12185  phimul  12239  eulerth  12246  pc2dvds  12342  pcz  12344  pcmpt  12354  pcmptdvds  12356  fldivp1  12359  oddprmdvds  12365  pockthg  12368  pockthi  12369  1arith  12378  zgz  12384  evenennn  12407  ennnfonelemp1  12420  ennnfonelemkh  12426  ennnfonelemnn0  12436  ssnnctlemct  12460  strslfv2  12519  strslfv  12520  ressvalsets  12537  ressbasid  12543  qusex  12763  xpsfeq  12782  intopsn  12804  mgmidmo  12809  ismgmid  12814  mgmlrid  12816  lidrideqd  12818  lidrididd  12819  grpinvalem  12822  grpinva  12823  issgrp  12827  mnd1  12868  mnd1id  12869  idmhm  12881  issubm  12884  0mhm  12894  dfgrp2  12923  isgrpid2  12936  grpidd2  12937  grpinvval  12939  grpressid  12957  grpsubid1  12981  dfgrp3mlem  12994  grplactfval  12997  imasgrp2  13004  mhmlem  13008  mulgfvalg  13015  mulgnnp1  13022  mulgsubcl  13028  mulgnncl  13029  mulgnn0cl  13030  mulgcl  13031  mulgnn0z  13041  mulgneg2  13048  mulgmodid  13053  issubg  13064  subgid  13066  subgex  13067  subg0  13071  subginv  13072  subgcl  13075  subgsub  13077  subgmulg  13079  issubg3  13083  isnsg  13093  isnsg3  13098  nmzsubg  13101  nmznsg  13104  eqgval  13114  ablressid  13169  mgpvalg  13173  rngressid  13204  ringressid  13306  imasring  13307  opprvalg  13312  opprsubgg  13327  dvdsrex  13341  dvdsrtr  13344  unitinvcl  13366  unitinvinv  13367  unitlinv  13369  unitrinv  13370  issubrng  13414  subrngid  13416  issubrng2  13425  issubrg  13436  subrgid  13438  issubrg2  13456  lmodlema  13476  islmodd  13477  rmodislmod  13535  lsssn0  13554  sraval  13621  sraring  13633  sralmod  13634  rlmvalg  13638  rlmbasg  13639  rlmplusgg  13640  rlm0g  13641  rlmsubg  13642  rlmmulrg  13643  rlmscabas  13644  rlmvscag  13645  rlmtopng  13646  rlmdsg  13647  rlmvnegg  13649  lidlss  13660  lidlssbas  13661  lidlbas  13662  zringinvg  13751  tsettps  13809  baspartn  13821  eltg  13823  en1top  13848  isopn3  13896  resttopon  13942  lmbr2  13985  cnptopresti  14009  cndis  14012  lmfpm  14014  lmcl  14016  lmff  14020  txswaphmeolem  14091  ispsmet  14094  psmet0  14098  xmetunirn  14129  bl2in  14174  metrest  14277  cncfmptid  14354  negcncf  14359  negfcncf  14360  limccl  14399  eldvap  14422  dvexp  14446  dveflem  14458  dvef  14459  logge0b  14582  logle1b  14584  logcxp  14589  zabsle1  14671  lgsval  14676  lgsfvalg  14677  lgsval2lem  14682  lgsdir2lem2  14701  lgsdir2lem4  14703  lgsdirnn0  14719  2lgsoddprmlem2  14725  2lgsoddprmlem3d  14729  bj-ex  14785  bdth  14854  bj-indind  14955