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  708  olc  713  orc  714  pm2.621  749  pm1.2  758  orim1i  762  orim2i  763  pm2.41  778  pm2.42  779  pm2.4  780  pm4.44  781  orim2  791  orbi1  794  pm2.38  805  pm2.74  809  pm3.2ni  815  biort  831  dcbiit  841  pm4.79dc  905  dcand  935  biantr  955  3anim1i  1188  3anim2i  1189  3anim3i  1190  mpd3an23  1352  trujust  1375  tru  1377  dftru2  1381  truimtru  1429  falimfal  1432  3impexp  1458  19.26  1505  19.8a  1614  19.9ht  1665  ax6blem  1674  19.36i  1696  19.41h  1709  equsb1  1809  sbieh  1814  dveeq2or  1840  spsbim  1867  2ax17  1902  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  moanmo  2133  nfcvf  2373  neqne  2386  neneq  2400  necon3i  2426  nebidc  2458  r19.27v  2635  r19.28v  2636  vtoclgft  2828  rspcime  2891  eueq2dc  2953  cdeqcv  2999  ru  3004  sbcied2  3043  sbcralt  3082  sbcrext  3083  csbiebt  3141  csbied2  3149  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  ssid  3221  difss2  3309  ddifstab  3313  abvor0dc  3492  ssdifeq0  3551  rabsnt  3718  unisng  3881  dfnfc2  3882  ssbr  4103  a9evsep  4182  axnul  4185  rabex2  4206  intid  4286  opm  4296  opth1  4298  opth  4299  copsex4g  4309  0nelop  4310  moop2  4314  pocl  4368  swopo  4371  limeq  4442  suceq  4467  eusvnfb  4519  onintexmid  4639  nn0eln0  4686  elvvuni  4757  coss1  4851  coss2  4852  dmxpm  4917  elrnmpt1  4948  soirri  5096  relcnvtr  5221  relssdmrn  5222  cnvpom  5244  fveqeq2  5608  funopsn  5785  fvsng  5803  isose  5913  canth  5920  riota2f  5944  acexmidlemab  5961  fvoveq1  5990  0neqopab  6013  ssoprab2  6024  caovcld  6123  caovcomd  6126  caovassd  6129  caovcand  6132  caovordid  6136  caovordd  6138  caovdid  6145  caovdird  6148  caovimo  6163  f1opw  6176  caofref  6206  caofinvl  6207  caofid0l  6208  caofid0r  6209  xpexgALT  6241  op1stg  6259  op2ndg  6260  releldm2  6294  elopabi  6304  dfmpo  6332  smoeq  6399  tfr1onlemaccex  6457  tfrcllemaccex  6470  rdgisucinc  6494  rdg0g  6497  oacl  6569  nna0r  6587  nnmsucr  6597  ercnv  6664  swoord1  6672  swoord2  6673  eqer  6675  ider  6676  iinerm  6717  brecop  6735  ixpssmapg  6838  elixpsn  6845  en1bg  6915  fundmeng  6923  rex2dom  6934  xpsneng  6942  mapen  6968  phplem3g  6978  php5  6980  php5dom  6985  findcard2d  7014  findcard2sd  7015  undifdc  7047  xpfi  7055  elfir  7101  fi0  7103  ordiso2  7163  ctssdclemr  7240  nnnninfeq2  7257  nninfisol  7261  ctssexmid  7278  nninfinfwlpo  7308  exmidaclem  7351  djuenun  7355  exmidapne  7407  cc1  7412  cc2lem  7413  mulidnq  7537  ltsonq  7546  halfnqq  7558  nqnq0pi  7586  nq02m  7613  cauappcvgprlemm  7793  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem2  7808  cauappcvgpr  7810  ltposr  7911  0idsr  7915  1idsr  7916  mappsrprg  7952  ax1rid  8025  ax0id  8026  axpre-ltirr  8030  mulrid  8104  1p1times  8241  cnegexlem3  8284  pncan1  8484  npcan1  8485  kcnktkm1cn  8490  apirr  8713  recexap  8761  eqneg  8840  subrecap  8947  lediv2a  9003  nn1m1nn  9089  2txmxeqx  9203  subhalfhalf  9307  add1p1  9322  sub1m1  9323  cnm2m1cnm3  9324  xp1d2m1eqxm1d2  9325  div4p1lem1div2  9326  nn0addcl  9365  nn0mulcl  9366  zadd2cl  9537  nn0ledivnn  9924  nltpnft  9971  ngtmnft  9974  xrrebnd  9976  xnegneg  9990  xnegid  10016  xaddid1  10019  fzss1  10220  fzssp1  10224  fzshftral  10265  0elfz  10275  nn0fz0  10276  elfz0add  10277  fz0tp  10279  elfzoelz  10304  fzoval  10305  fzoss2  10331  fzossrbm1  10332  fzouzsplit  10338  elfzo1  10351  fzonn0p1  10377  fzossfzop1  10378  fzoend  10388  fzosplitsn  10399  fvinim0ffz  10407  2tnp1ge0ge0  10481  fldiv4p1lem1div2  10485  frec2uzltd  10585  frec2uzrand  10587  uzenom  10607  frecfzennn  10608  seqeq1  10632  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemqk  10689  seq3f1olemstep  10696  seq3f1olemp  10697  seq3f1oleml  10698  seqf1oglem2  10702  seq3id  10707  seq3id2  10708  ser0f  10716  m1expcl2  10743  sqoddm1div8  10875  mulsubdivbinom2ap  10893  faclbnd  10923  facubnd  10927  bcpasc  10948  hashcl  10963  omgadd  10984  snopiswrd  11041  elovmpowrd  11072  lswwrd  11077  ccatval1  11091  ccatsymb  11096  ccatass  11102  ccat1st1st  11131  swrdf  11146  pfxsuff1eqwrdeq  11190  ccatpfx  11192  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  swrdccatin2d  11235  reuccatpfxs1lem  11237  reval  11275  imval  11276  crim  11284  replim  11285  rexuz3  11416  absval  11427  sqrt0  11430  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrex  11452  abs00  11490  leabs  11500  absimle  11510  cau3  11541  dfabsmax  11643  climshft  11730  fsum3  11813  fsumcnv  11863  fsumiun  11903  binom  11910  bcxmaslem1  11914  isumshft  11916  arisum  11924  arisum2  11925  trireciplem  11926  trirecip  11927  geo2sum2  11941  geo2lim  11942  prodf1f  11969  prod0  12011  fprodfac  12041  ege2le3  12097  ef4p  12120  efgt1p2  12121  efgt1p  12122  sinval  12128  cosval  12129  negdvdsb  12233  dvdsnegb  12234  dvdsssfz1  12278  dvds1  12279  3dvds  12290  even2n  12300  oddge22np1  12307  2tp1odd  12310  ltoddhalfle  12319  m1expo  12326  m1exp1  12327  flodddiv4  12362  bits0e  12375  bits0o  12376  bitsp1e  12378  bitsp1o  12379  bitsfzo  12381  bitsinv1lem  12387  bitsinv1  12388  gcdsupex  12393  gcdsupcl  12394  alginv  12484  algcvg  12485  algcvga  12488  algfx  12489  eucalgcvga  12495  lcmdvds  12516  pw2dvds  12603  oddpwdclemodd  12609  phimul  12663  eulerth  12670  pc2dvds  12768  pcz  12770  pcmpt  12781  pcmptdvds  12783  fldivp1  12786  oddprmdvds  12792  pockthg  12795  pockthi  12796  1arith  12805  zgz  12811  4sqlem19  12847  evenennn  12879  ennnfonelemp1  12892  ennnfonelemkh  12898  ennnfonelemnn0  12908  ssnnctlemct  12932  strslfv2  12991  strslfv  12992  basm  13008  ressvalsets  13011  ressbasid  13017  pwsval  13238  qusex  13272  xpsfeq  13292  intopsn  13314  mgmidmo  13319  ismgmid  13324  mgmlrid  13326  lidrideqd  13328  lidrididd  13329  grpinvalem  13332  grpinva  13333  gsum0g  13343  issgrp  13350  imasmnd2  13399  mnd1  13402  mnd1id  13403  idmhm  13416  issubm  13419  0mhm  13433  resmhm  13434  resmhm2  13435  resmhm2b  13436  dfgrp2  13474  isgrpid2  13487  grpidd2  13488  grpinvval  13490  grpressid  13508  grpsubid1  13532  dfgrp3mlem  13545  grplactfval  13548  imasgrp2  13561  mhmlem  13565  mulgfvalg  13572  mulgnnp1  13581  mulgsubcl  13587  mulgnncl  13588  mulgnn0cl  13589  mulgcl  13590  mulgnn0z  13600  mulgneg2  13607  mulgmodid  13612  submmulg  13617  issubg  13624  subgid  13626  subgex  13627  subg0  13631  subginv  13632  subgcl  13635  subgsub  13637  subgmulg  13639  issubg3  13643  isnsg  13653  isnsg3  13658  nmzsubg  13661  nmznsg  13664  eqgval  13674  idghm  13710  resghm  13711  ghmnsgima  13719  ablressid  13786  mgpvalg  13800  rngressid  13831  ringressid  13940  imasring  13941  opprvalg  13946  opprsubgg  13961  dvdsrex  13975  dvdsrtr  13978  unitinvcl  14000  unitinvinv  14001  unitlinv  14003  unitrinv  14004  issubrng  14076  subrngid  14078  issubrng2  14087  issubrg  14098  subrgid  14100  issubrg2  14118  rrgval  14139  isdomn  14146  lmodlema  14169  islmodd  14170  rmodislmod  14228  lsssn0  14247  sraval  14314  sraring  14326  sralmod  14327  rlmvalg  14331  rlmbasg  14332  rlmplusgg  14333  rlm0g  14334  rlmsubg  14335  rlmmulrg  14336  rlmscabas  14337  rlmvscag  14338  rlmtopng  14339  rlmdsg  14340  rlmvnegg  14342  lidlss  14353  lidlssbas  14354  lidlbas  14355  crngridl  14407  zringinvg  14481  mulgrhm  14486  znval  14513  znf1o  14528  psrelbasfun  14554  mplvalcoe  14567  tsettps  14625  baspartn  14637  eltg  14639  en1top  14664  isopn3  14712  resttopon  14758  lmbr2  14801  cnptopresti  14825  cndis  14828  lmfpm  14830  lmcl  14832  lmff  14836  txswaphmeolem  14907  ispsmet  14910  psmet0  14914  xmetunirn  14945  bl2in  14990  metrest  15093  expcn  15156  cncfmptid  15184  negcncf  15192  negfcncf  15193  hovera  15234  hoverb  15235  limccl  15246  eldvap  15269  dvexp  15298  dvmptid  15303  dveflem  15313  dvef  15314  elply  15321  plypow  15331  dvply1  15352  logge0b  15477  logle1b  15479  logcxp  15484  fsumdvdsmul  15578  perfectlem2  15587  zabsle1  15591  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdirnn0  15639  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2dlem1  15653  2lgslem1a1  15678  2lgslem1a2  15679  2lgslem1b  15681  2lgslem1c  15682  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgsoddprmlem2  15698  2lgsoddprmlem3d  15702  edgfndxid  15723  uhgr0e  15793  umgrislfupgrdom  15837  bj-ex  15898  bdth  15966  bj-indind  16067