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  599  pm5.36  612  con2i  630  notnot  632  con3i  635  biijust  644  con3  645  con2  646  pm5.19  711  olc  716  orc  717  pm2.621  752  pm1.2  761  orim1i  765  orim2i  766  pm2.41  781  pm2.42  782  pm2.4  783  pm4.44  784  orim2  794  orbi1  797  pm2.38  808  pm2.74  812  pm3.2ni  818  biort  834  dcbiit  844  pm4.79dc  908  dcand  938  biantr  958  3anim1i  1209  3anim2i  1210  3anim3i  1211  mpd3an23  1373  trujust  1397  tru  1399  dftru2  1403  truimtru  1451  falimfal  1454  3impexp  1480  19.26  1527  19.8a  1636  19.9ht  1687  ax6blem  1696  19.36i  1718  19.41h  1731  equsb1  1831  sbieh  1836  dveeq2or  1862  spsbim  1889  2ax17  1924  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  moanmo  2155  nfcvf  2395  neqne  2408  neneq  2422  necon3i  2448  nebidc  2480  r19.27v  2658  r19.28v  2659  vtoclgft  2851  rspcime  2914  eueq2dc  2976  cdeqcv  3022  ru  3027  sbcied2  3066  sbcralt  3105  sbcrext  3106  csbiebt  3164  csbied2  3172  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ssid  3244  difss2  3332  ddifstab  3336  abvor0dc  3515  ssdifeq0  3574  rabsnt  3741  unisng  3905  dfnfc2  3906  ssbr  4127  a9evsep  4206  axnul  4209  rabex2  4230  intid  4310  opm  4320  opth1  4322  opth  4323  copsex4g  4333  0nelop  4334  moop2  4338  pocl  4394  swopo  4397  limeq  4468  suceq  4493  eusvnfb  4545  onintexmid  4665  nn0eln0  4712  elvvuni  4783  coss1  4877  coss2  4878  dmxpm  4944  elrnmpt1  4975  soirri  5123  relcnvtr  5248  relssdmrn  5249  cnvpom  5271  fveqeq2  5638  funopsn  5819  fvsng  5839  isose  5951  canth  5958  riota2f  5983  riotaeqimp  5985  acexmidlemab  6001  fvoveq1  6030  0neqopab  6055  ssoprab2  6066  caovcld  6165  caovcomd  6168  caovassd  6171  caovcand  6174  caovordid  6178  caovordd  6180  caovdid  6187  caovdird  6190  caovimo  6205  f1opw  6219  caofref  6249  caofinvl  6250  caofid0l  6251  caofid0r  6252  xpexgALT  6284  op1stg  6302  op2ndg  6303  releldm2  6337  elopabi  6347  dfmpo  6375  smoeq  6442  tfr1onlemaccex  6500  tfrcllemaccex  6513  rdgisucinc  6537  rdg0g  6540  oacl  6614  nna0r  6632  nnmsucr  6642  ercnv  6709  swoord1  6717  swoord2  6718  eqer  6720  ider  6721  iinerm  6762  brecop  6780  ixpssmapg  6883  elixpsn  6890  en1bg  6960  fundmeng  6968  rex2dom  6979  xpsneng  6989  mapen  7015  phplem3g  7025  php5  7027  php5dom  7032  findcard2d  7061  findcard2sd  7062  undifdc  7097  xpfi  7105  elfir  7151  fi0  7153  ordiso2  7213  ctssdclemr  7290  nnnninfeq2  7307  nninfisol  7311  ctssexmid  7328  nninfinfwlpo  7358  exmidaclem  7401  djuenun  7405  exmidapne  7457  cc1  7462  cc2lem  7463  mulidnq  7587  ltsonq  7596  halfnqq  7608  nqnq0pi  7636  nq02m  7663  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  cauappcvgpr  7860  ltposr  7961  0idsr  7965  1idsr  7966  mappsrprg  8002  ax1rid  8075  ax0id  8076  axpre-ltirr  8080  mulrid  8154  1p1times  8291  cnegexlem3  8334  pncan1  8534  npcan1  8535  kcnktkm1cn  8540  apirr  8763  recexap  8811  eqneg  8890  subrecap  8997  lediv2a  9053  nn1m1nn  9139  2txmxeqx  9253  subhalfhalf  9357  add1p1  9372  sub1m1  9373  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  nn0addcl  9415  nn0mulcl  9416  zadd2cl  9587  nn0ledivnn  9975  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xnegneg  10041  xnegid  10067  xaddid1  10070  fzss1  10271  fzssp1  10275  fzshftral  10316  0elfz  10326  nn0fz0  10327  elfz0add  10328  fz0tp  10330  elfzoelz  10355  fzoval  10356  fzoss2  10382  fzossrbm1  10383  fzouzsplit  10389  elfzo1  10403  fzonn0p1  10429  fzossfzop1  10430  fzoend  10440  fzosplitsn  10451  fvinim0ffz  10459  2tnp1ge0ge0  10533  fldiv4p1lem1div2  10537  frec2uzltd  10637  frec2uzrand  10639  uzenom  10659  frecfzennn  10660  seqeq1  10684  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqk  10741  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem2  10754  seq3id  10759  seq3id2  10760  ser0f  10768  m1expcl2  10795  sqoddm1div8  10927  mulsubdivbinom2ap  10945  faclbnd  10975  facubnd  10979  bcpasc  11000  hashcl  11015  omgadd  11036  snopiswrd  11094  elovmpowrd  11126  lswwrd  11131  ccatval1  11145  ccatsymb  11150  ccatass  11156  ccat1st1st  11188  swrdf  11203  pfxsuff1eqwrdeq  11247  ccatpfx  11249  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12  11281  swrdccatin2d  11292  reuccatpfxs1lem  11294  s3eq2  11325  reval  11376  imval  11377  crim  11385  replim  11386  rexuz3  11517  absval  11528  sqrt0  11531  resqrexlemp1rp  11533  resqrexlemfp1  11536  resqrex  11553  abs00  11591  leabs  11601  absimle  11611  cau3  11642  dfabsmax  11744  climshft  11831  fsum3  11914  fsumcnv  11964  fsumiun  12004  binom  12011  bcxmaslem1  12015  isumshft  12017  arisum  12025  arisum2  12026  trireciplem  12027  trirecip  12028  geo2sum2  12042  geo2lim  12043  prodf1f  12070  prod0  12112  fprodfac  12142  ege2le3  12198  ef4p  12221  efgt1p2  12222  efgt1p  12223  sinval  12229  cosval  12230  negdvdsb  12334  dvdsnegb  12335  dvdsssfz1  12379  dvds1  12380  3dvds  12391  even2n  12401  oddge22np1  12408  2tp1odd  12411  ltoddhalfle  12420  m1expo  12427  m1exp1  12428  flodddiv4  12463  bits0e  12476  bits0o  12477  bitsp1e  12479  bitsp1o  12480  bitsfzo  12482  bitsinv1lem  12488  bitsinv1  12489  gcdsupex  12494  gcdsupcl  12495  alginv  12585  algcvg  12586  algcvga  12589  algfx  12590  eucalgcvga  12596  lcmdvds  12617  pw2dvds  12704  oddpwdclemodd  12710  phimul  12764  eulerth  12771  pc2dvds  12869  pcz  12871  pcmpt  12882  pcmptdvds  12884  fldivp1  12887  oddprmdvds  12893  pockthg  12896  pockthi  12897  1arith  12906  zgz  12912  4sqlem19  12948  evenennn  12980  ennnfonelemp1  12993  ennnfonelemkh  12999  ennnfonelemnn0  13009  ssnnctlemct  13033  strslfv2  13092  strslfv  13093  basm  13110  ressvalsets  13113  ressbasid  13119  pwsval  13340  qusex  13374  xpsfeq  13394  intopsn  13416  mgmidmo  13421  ismgmid  13426  mgmlrid  13428  lidrideqd  13430  lidrididd  13431  grpinvalem  13434  grpinva  13435  gsum0g  13445  issgrp  13452  imasmnd2  13501  mnd1  13504  mnd1id  13505  idmhm  13518  issubm  13521  0mhm  13535  resmhm  13536  resmhm2  13537  resmhm2b  13538  dfgrp2  13576  isgrpid2  13589  grpidd2  13590  grpinvval  13592  grpressid  13610  grpsubid1  13634  dfgrp3mlem  13647  grplactfval  13650  imasgrp2  13663  mhmlem  13667  mulgfvalg  13674  mulgnnp1  13683  mulgsubcl  13689  mulgnncl  13690  mulgnn0cl  13691  mulgcl  13692  mulgnn0z  13702  mulgneg2  13709  mulgmodid  13714  submmulg  13719  issubg  13726  subgid  13728  subgex  13729  subg0  13733  subginv  13734  subgcl  13737  subgsub  13739  subgmulg  13741  issubg3  13745  isnsg  13755  isnsg3  13760  nmzsubg  13763  nmznsg  13766  eqgval  13776  idghm  13812  resghm  13813  ghmnsgima  13821  ablressid  13888  mgpvalg  13902  rngressid  13933  ringressid  14042  imasring  14043  opprvalg  14048  opprsubgg  14063  dvdsrex  14078  dvdsrtr  14081  unitinvcl  14103  unitinvinv  14104  unitlinv  14106  unitrinv  14107  issubrng  14179  subrngid  14181  issubrng2  14190  issubrg  14201  subrgid  14203  issubrg2  14221  rrgval  14242  isdomn  14249  lmodlema  14272  islmodd  14273  rmodislmod  14331  lsssn0  14350  sraval  14417  sraring  14429  sralmod  14430  rlmvalg  14434  rlmbasg  14435  rlmplusgg  14436  rlm0g  14437  rlmsubg  14438  rlmmulrg  14439  rlmscabas  14440  rlmvscag  14441  rlmtopng  14442  rlmdsg  14443  rlmvnegg  14445  lidlss  14456  lidlssbas  14457  lidlbas  14458  crngridl  14510  zringinvg  14584  mulgrhm  14589  znval  14616  znf1o  14631  psrelbasfun  14657  mplvalcoe  14670  tsettps  14728  baspartn  14740  eltg  14742  en1top  14767  isopn3  14815  resttopon  14861  lmbr2  14904  cnptopresti  14928  cndis  14931  lmfpm  14933  lmcl  14935  lmff  14939  txswaphmeolem  15010  ispsmet  15013  psmet0  15017  xmetunirn  15048  bl2in  15093  metrest  15196  expcn  15259  cncfmptid  15287  negcncf  15295  negfcncf  15296  hovera  15337  hoverb  15338  limccl  15349  eldvap  15372  dvexp  15401  dvmptid  15406  dveflem  15416  dvef  15417  elply  15424  plypow  15434  dvply1  15455  logge0b  15580  logle1b  15582  logcxp  15587  fsumdvdsmul  15681  perfectlem2  15690  zabsle1  15694  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsdir2lem2  15724  lgsdir2lem4  15726  lgsdirnn0  15742  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem1  15756  2lgslem1a1  15781  2lgslem1a2  15782  2lgslem1b  15784  2lgslem1c  15785  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgsoddprmlem2  15801  2lgsoddprmlem3d  15805  edgfndxid  15826  uhgr0e  15898  umgrislfupgrdom  15945  ausgrusgrien  15985  clwwlkext2edg  16164  clwwlknccat  16165  bj-ex  16209  bdth  16277  bj-indind  16378