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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  399  anass  405  mpdan  425  mpancom  426  pm5.32  457  anbi1  470  anbi2  471  mpan10  478  adantl3r  516  simpll  531  simplr  533  simprl  535  simprr  537  pm3.45  605  pm5.36  618  con2i  636  notnot  638  con3i  641  biijust  650  con3  651  con2  652  pm5.19  718  olc  723  orc  724  pm2.621  759  pm1.2  768  orim1i  772  orim2i  773  pm2.41  788  pm2.42  789  pm2.4  790  pm4.44  791  orim2  801  orbi1  804  pm2.38  815  pm2.74  819  pm3.2ni  825  biort  841  dcbiit  851  pm4.79dc  915  dcand  945  biantr  965  3anim1i  1216  3anim2i  1217  3anim3i  1218  mpd3an23  1380  trujust  1404  tru  1406  dftru2  1410  truimtru  1458  falimfal  1461  3impexp  1487  19.26  1534  19.8a  1643  19.9ht  1694  hbn  1703  19.36i  1724  19.41h  1737  equsb1  1838  sbieh  1843  dveeq2or  1869  spsbim  1896  2ax17  1931  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  moanmo  2164  nfcvf  2415  neqne  2428  neneq  2442  necon3i  2468  nebidc  2500  r19.27v  2678  r19.28v  2679  vtoclgft  2873  rspcime  2937  eueq2dc  2999  cdeqcv  3045  ru  3050  sbcied2  3089  sbcralt  3128  sbcrext  3129  csbiebt  3187  csbied2  3195  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ssid  3268  difss2  3357  ddifstab  3361  abvor0dc  3545  ssdifeq0  3610  rabsnt  3786  unisng  3952  dfnfc2  3953  ssbr  4175  a9evsep  4257  axnul  4260  sepab  4280  rabex2  4284  intid  4366  opm  4376  opth1  4378  opth  4379  copsex4g  4389  0nelop  4390  moop2  4394  pocl  4450  swopo  4453  limeq  4524  suceq  4549  eusvnfb  4602  onintexmid  4722  nn0eln0  4769  elvvuni  4841  coss1  4937  coss2  4938  dmxpm  5004  elrnmpt1  5035  soirri  5185  relcnvtr  5310  relssdmrn  5311  cnvpom  5333  fveqeq2  5707  fsn2g  5886  funopsn  5894  fvsng  5914  isose  6030  canth  6039  riota2f  6064  riotaeqimp  6066  acexmidlemab  6082  fvoveq1  6111  0neqopab  6136  ssoprab2  6147  caovcld  6246  caovcomd  6249  caovassd  6252  caovcand  6255  caovordid  6259  caovordd  6261  caovdid  6268  caovdird  6271  caovimo  6286  f1opw  6300  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  xpexgALT  6370  op1stg  6388  op2ndg  6389  releldm2  6423  opabn1stprc  6433  elopabi  6435  dfmpo  6463  smoeq  6565  tfr1onlemaccex  6623  tfrcllemaccex  6636  rdgisucinc  6660  rdg0g  6663  oacl  6737  nna0r  6755  nnmsucr  6765  ercnv  6832  swoord1  6840  swoord2  6841  eqer  6843  ider  6844  iinerm  6885  brecop  6903  fsetdmprc0  6954  ixpssmapg  7014  elixpsn  7021  en1bg  7091  fundmeng  7099  rex2dom  7114  xpsneng  7124  mapen  7150  phplem3g  7161  php5  7163  php5dom  7168  findcard2d  7199  findcard2sd  7200  undifdc  7235  xpfi  7243  fsuppxpfi  7301  elfir  7312  fi0  7314  ordiso2  7381  ctssdclemr  7458  nnnninfeq2  7475  nninfisol  7479  ctssexmid  7496  nninfinfwlpo  7526  exmidaclem  7570  djuenun  7574  papeq2  7616  papirr  7617  exmidapne  7632  cc1  7637  cc2lem  7638  mulidnq  7762  ltsonq  7771  halfnqq  7783  nqnq0pi  7811  nq02m  7838  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  cauappcvgpr  8035  ltposr  8136  0idsr  8140  1idsr  8141  mappsrprg  8177  ax1rid  8250  ax0id  8251  axpre-ltirr  8255  mulrid  8329  1p1times  8467  cnegexlem3  8510  pncan1  8711  npcan1  8712  kcnktkm1cn  8717  apirr  8941  recexap  8989  msq0  9005  eqneg  9070  subrecap  9177  lediv2a  9233  nn1m1nn  9331  2txmxeqx  9445  subhalfhalf  9551  add1p1  9566  sub1m1  9567  cnm2m1cnm3  9568  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  nn0addcl  9609  nn0mulcl  9610  zadd2cl  9786  nn0ledivnn  10185  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xnegneg  10252  xnegid  10278  xaddid1  10281  fzss1  10486  fzssp1  10490  fzshftral  10532  0elfz  10542  nn0fz0  10543  elfz0add  10544  fz0tp  10546  elfzoelz  10571  fzoval  10572  fzoss2  10598  fzossrbm1  10599  fzouzsplit  10605  elfzo1  10620  fzonn0p1  10646  fzossfzop1  10647  fzoend  10657  fzosplitsn  10668  fvinim0ffz  10677  2tnp1ge0ge0  10757  fldiv4p1lem1div2  10761  frec2uzltd  10861  frec2uzrand  10863  uzenom  10883  frecfzennn  10884  seqeq1  10908  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqk  10965  seq3f1olemstep  10972  seq3f1olemp  10973  seq3f1oleml  10974  seqf1oglem2  10978  seq3id  10983  seq3id2  10984  ser0f  10992  m1expcl2  11019  resq01  11116  sqoddm1div8  11152  mulsubdivbinom2ap  11171  faclbnd  11201  facubnd  11205  bcpasc  11226  hashcl  11242  omgadd  11264  hashfibc  11305  snopiswrd  11336  elovmpowrd  11368  lswwrd  11373  ccatval1  11387  ccatsymb  11392  ccatass  11398  ccat1st1st  11431  swrdf  11449  pfxsuff1eqwrdeq  11493  ccatpfx  11495  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccatin2d  11538  reuccatpfxs1lem  11540  s3eq2  11571  reval  11636  imval  11637  crim  11645  replim  11646  sq01  11682  rexuz3  11778  absval  11789  sqrt0  11792  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrex  11814  abs00  11852  leabs  11862  absimle  11873  cau3  11904  dfabsmax  12006  climshft  12095  fsum3  12179  fsumcnv  12229  fsumiun  12269  binom  12276  bcxmaslem1  12280  isumshft  12282  arisum  12290  arisum2  12291  trireciplem  12292  trirecip  12293  geo2sum2  12307  geo2lim  12308  prodf1f  12335  prod0  12377  fprodfac  12407  ege2le3  12463  ef4p  12486  efgt1p2  12487  efgt1p  12488  sinval  12494  cosval  12495  negdvdsb  12599  dvdsnegb  12600  dvdsssfz1  12644  dvds1  12645  3dvds  12656  even2n  12666  oddge22np1  12673  2tp1odd  12676  ltoddhalfle  12685  m1expo  12692  m1exp1  12693  flodddiv4  12728  bits0e  12741  bits0o  12742  bitsp1e  12744  bitsp1o  12745  bitsfzo  12747  bitsinv1lem  12753  bitsinv1  12754  gcdsupex  12759  gcdsupcl  12760  alginv  12850  algcvg  12851  algcvga  12854  algfx  12855  eucalgcvga  12861  lcmdvds  12882  phimul  13033  eulerth  13040  pc2dvds  13138  pcz  13140  pcmpt  13151  pcmptdvds  13153  fldivp1  13156  oddprmdvds  13162  pockthg  13165  pockthi  13166  1arith  13175  zgz  13181  4sqlem19  13217  ballotfilemfmpn  13292  ballotfilemfval0  13293  ballotfilemsv  13311  ballotfilemsf1o  13315  ballotfilemrval  13319  ballotfilemro  13324  ballotfilemrinv  13335  ballotfi  13340  evenennn  13342  ennnfonelemp1  13355  ennnfonelemkh  13361  ennnfonelemnn0  13371  ssnnctlemct  13395  strslfv2  13454  strslfv  13455  basm  13472  slotm  13473  ressvalsets  13476  ressbasid  13483  qusex  13705  xpsfeq  13725  intopsn  13746  mgmidmo  13751  ismgmid  13756  mgmlrid  13758  lidrideqd  13760  lidrididd  13761  grpinvalem  13764  grpinva  13765  gzsum0  13772  issgrp  13777  imasmnd2  13818  mnd1  13821  mnd1id  13822  idmhm  13835  issubm  13838  0mhm  13852  resmhm  13853  resmhm2  13854  resmhm2b  13855  dfgrp2  13891  isgrpid2  13904  grpidd2  13905  grpinvval  13907  grpressid  13925  grpsubid1  13949  dfgrp3mlem  13962  grplactfval  13965  imasgrp2  13972  mhmlem  13976  mulgfvalg  13983  mulgnnp1  13992  mulgsubcl  13998  mulgnncl  13999  mulgnn0cl  14000  mulgcl  14001  mulgnn0z  14011  mulgneg2  14018  mulgmodid  14023  submmulg  14028  issubg  14035  subgid  14037  subgex  14038  subg0  14042  subginv  14043  subgcl  14046  subgsub  14048  subgmulg  14050  issubg3  14054  isnsg  14064  isnsg3  14069  nmzsubg  14072  nmznsg  14075  eqgval  14085  idghm  14121  resghm  14122  ghmnsgima  14130  cntrval  14151  cntzssv  14160  ablressid  14229  gsum0cmn  14244  pwsval  14311  mgpvalg  14327  rngressid  14360  ringressid  14477  imasring  14478  opprvalg  14483  opprsubgg  14499  dvdsrex  14514  dvdsrtr  14517  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  opprlring  14613  issubrng  14616  subrngid  14618  issubrng2  14627  issubrg  14638  subrgid  14640  issubrg2  14658  rrgval  14679  isdomn  14687  aprprop  14710  drnggrp  14722  opprdrng  14729  lmodlema  14737  islmodd  14738  rmodislmod  14797  lsssn0  14816  sraval  14883  sraring  14895  sralmod  14896  rlmvalg  14900  rlmbasg  14901  rlmplusgg  14902  rlm0g  14903  rlmsubg  14904  rlmmulrg  14905  rlmscabas  14906  rlmvscag  14907  rlmtopng  14908  rlmdsg  14909  rlmvnegg  14911  lidlss  14922  lidlssbas  14923  lidlbas  14924  crngridl  14976  zringinvg  15048  mulgrhm  15053  znval  15080  znf1o  15095  aspval  15124  asclfval  15130  psrbagfsupp  15164  psrbaglesupp  15167  psrbaglecl  15169  psrbagcon  15171  psrelbasfun  15181  mplvalcoe  15206  tsettps  15264  baspartn  15276  eltg  15278  en1top  15303  isopn3  15351  resttopon  15397  lmbr2  15440  cnptopresti  15464  cndis  15467  lmfpm  15469  lmcl  15471  lmff  15475  txswaphmeolem  15546  ispsmet  15549  psmet0  15553  xmetunirn  15584  bl2in  15629  metrest  15732  expcn  15795  cncfmptid  15823  negcncf  15831  negfcncf  15832  hovera  15873  hoverb  15874  limccl  15885  eldvap  15908  dvexp  15937  dvmptid  15942  dveflem  15952  dvef  15953  elply  15960  plypow  15970  dvply1  15991  efap1p  16005  logge0b  16120  logle1b  16122  logfac  16126  logcxp  16130  log2tlbndlog2  16220  chtdif  16264  ppidif  16269  ppiqltx  16281  prmorcht  16282  fsumdvdsmul  16285  chtublem  16295  chtqub  16296  perfectlem2  16300  bclbnd  16307  bposlem3  16313  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  zabsle1  16323  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdirnn0  16371  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  gausslemma2dlem1  16385  2lgslem1a1  16410  2lgslem1a2  16411  2lgslem1b  16413  2lgslem1c  16414  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgsoddprmlem2  16430  2lgsoddprmlem3d  16434  edgfndxid  16455  uhgr0e  16528  umgrislfupgrdom  16577  ausgrusgrien  16617  egrsubgr  16709  uhgrsubgrself  16712  uhgrspanop  16728  clwwlkext2edg  16868  clwwlknccat  16869  clwwlknonmpo  16874  iseupth  16893  bj-ex  16995  bdth  17062  bj-indind  17163  exmidcon  17242  exmidpeirce  17243