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  529  simprl  531  simprr  533  pm3.45  601  pm5.36  614  con2i  632  notnot  634  con3i  637  biijust  646  con3  647  con2  648  pm5.19  713  olc  718  orc  719  pm2.621  754  pm1.2  763  orim1i  767  orim2i  768  pm2.41  783  pm2.42  784  pm2.4  785  pm4.44  786  orim2  796  orbi1  799  pm2.38  810  pm2.74  814  pm3.2ni  820  biort  836  dcbiit  846  pm4.79dc  910  dcand  940  biantr  960  3anim1i  1211  3anim2i  1212  3anim3i  1213  mpd3an23  1375  trujust  1399  tru  1401  dftru2  1405  truimtru  1453  falimfal  1456  3impexp  1482  19.26  1529  19.8a  1638  19.9ht  1689  ax6blem  1698  19.36i  1720  19.41h  1733  equsb1  1833  sbieh  1838  dveeq2or  1864  spsbim  1891  2ax17  1926  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  moanmo  2157  nfcvf  2397  neqne  2410  neneq  2424  necon3i  2450  nebidc  2482  r19.27v  2660  r19.28v  2661  vtoclgft  2854  rspcime  2917  eueq2dc  2979  cdeqcv  3025  ru  3030  sbcied2  3069  sbcralt  3108  sbcrext  3109  csbiebt  3167  csbied2  3175  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  ssid  3247  difss2  3335  ddifstab  3339  abvor0dc  3518  ssdifeq0  3577  rabsnt  3746  unisng  3910  dfnfc2  3911  ssbr  4132  a9evsep  4211  axnul  4214  rabex2  4236  intid  4316  opm  4326  opth1  4328  opth  4329  copsex4g  4339  0nelop  4340  moop2  4344  pocl  4400  swopo  4403  limeq  4474  suceq  4499  eusvnfb  4551  onintexmid  4671  nn0eln0  4718  elvvuni  4790  coss1  4885  coss2  4886  dmxpm  4952  elrnmpt1  4983  soirri  5131  relcnvtr  5256  relssdmrn  5257  cnvpom  5279  fveqeq2  5648  fsn2g  5822  funopsn  5830  fvsng  5850  isose  5962  canth  5969  riota2f  5994  riotaeqimp  5996  acexmidlemab  6012  fvoveq1  6041  0neqopab  6066  ssoprab2  6077  caovcld  6176  caovcomd  6179  caovassd  6182  caovcand  6185  caovordid  6189  caovordd  6191  caovdid  6198  caovdird  6201  caovimo  6216  f1opw  6230  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  xpexgALT  6295  op1stg  6313  op2ndg  6314  releldm2  6348  opabn1stprc  6358  elopabi  6360  dfmpo  6388  smoeq  6456  tfr1onlemaccex  6514  tfrcllemaccex  6527  rdgisucinc  6551  rdg0g  6554  oacl  6628  nna0r  6646  nnmsucr  6656  ercnv  6723  swoord1  6731  swoord2  6732  eqer  6734  ider  6735  iinerm  6776  brecop  6794  ixpssmapg  6897  elixpsn  6904  en1bg  6974  fundmeng  6982  rex2dom  6996  xpsneng  7006  mapen  7032  phplem3g  7042  php5  7044  php5dom  7049  findcard2d  7080  findcard2sd  7081  undifdc  7116  xpfi  7124  elfir  7172  fi0  7174  ordiso2  7234  ctssdclemr  7311  nnnninfeq2  7328  nninfisol  7332  ctssexmid  7349  nninfinfwlpo  7379  exmidaclem  7423  djuenun  7427  exmidapne  7479  cc1  7484  cc2lem  7485  mulidnq  7609  ltsonq  7618  halfnqq  7630  nqnq0pi  7658  nq02m  7685  cauappcvgprlemm  7865  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  cauappcvgpr  7882  ltposr  7983  0idsr  7987  1idsr  7988  mappsrprg  8024  ax1rid  8097  ax0id  8098  axpre-ltirr  8102  mulrid  8176  1p1times  8313  cnegexlem3  8356  pncan1  8556  npcan1  8557  kcnktkm1cn  8562  apirr  8785  recexap  8833  eqneg  8912  subrecap  9019  lediv2a  9075  nn1m1nn  9161  2txmxeqx  9275  subhalfhalf  9379  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  nn0addcl  9437  nn0mulcl  9438  zadd2cl  9609  nn0ledivnn  10002  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xnegneg  10068  xnegid  10094  xaddid1  10097  fzss1  10298  fzssp1  10302  fzshftral  10343  0elfz  10353  nn0fz0  10354  elfz0add  10355  fz0tp  10357  elfzoelz  10382  fzoval  10383  fzoss2  10409  fzossrbm1  10410  fzouzsplit  10416  elfzo1  10431  fzonn0p1  10457  fzossfzop1  10458  fzoend  10468  fzosplitsn  10479  fvinim0ffz  10488  2tnp1ge0ge0  10562  fldiv4p1lem1div2  10566  frec2uzltd  10666  frec2uzrand  10668  uzenom  10688  frecfzennn  10689  seqeq1  10713  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqk  10770  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem2  10783  seq3id  10788  seq3id2  10789  ser0f  10797  m1expcl2  10824  sqoddm1div8  10956  mulsubdivbinom2ap  10974  faclbnd  11004  facubnd  11008  bcpasc  11029  hashcl  11044  omgadd  11066  snopiswrd  11127  elovmpowrd  11159  lswwrd  11164  ccatval1  11178  ccatsymb  11183  ccatass  11189  ccat1st1st  11222  swrdf  11240  pfxsuff1eqwrdeq  11284  ccatpfx  11286  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccatin2d  11329  reuccatpfxs1lem  11331  s3eq2  11362  reval  11427  imval  11428  crim  11436  replim  11437  rexuz3  11568  absval  11579  sqrt0  11582  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrex  11604  abs00  11642  leabs  11652  absimle  11662  cau3  11693  dfabsmax  11795  climshft  11882  fsum3  11966  fsumcnv  12016  fsumiun  12056  binom  12063  bcxmaslem1  12067  isumshft  12069  arisum  12077  arisum2  12078  trireciplem  12079  trirecip  12080  geo2sum2  12094  geo2lim  12095  prodf1f  12122  prod0  12164  fprodfac  12194  ege2le3  12250  ef4p  12273  efgt1p2  12274  efgt1p  12275  sinval  12281  cosval  12282  negdvdsb  12386  dvdsnegb  12387  dvdsssfz1  12431  dvds1  12432  3dvds  12443  even2n  12453  oddge22np1  12460  2tp1odd  12463  ltoddhalfle  12472  m1expo  12479  m1exp1  12480  flodddiv4  12515  bits0e  12528  bits0o  12529  bitsp1e  12531  bitsp1o  12532  bitsfzo  12534  bitsinv1lem  12540  bitsinv1  12541  gcdsupex  12546  gcdsupcl  12547  alginv  12637  algcvg  12638  algcvga  12641  algfx  12642  eucalgcvga  12648  lcmdvds  12669  pw2dvds  12756  oddpwdclemodd  12762  phimul  12816  eulerth  12823  pc2dvds  12921  pcz  12923  pcmpt  12934  pcmptdvds  12936  fldivp1  12939  oddprmdvds  12945  pockthg  12948  pockthi  12949  1arith  12958  zgz  12964  4sqlem19  13000  evenennn  13032  ennnfonelemp1  13045  ennnfonelemkh  13051  ennnfonelemnn0  13061  ssnnctlemct  13085  strslfv2  13144  strslfv  13145  basm  13162  ressvalsets  13165  ressbasid  13171  pwsval  13392  qusex  13426  xpsfeq  13446  intopsn  13468  mgmidmo  13473  ismgmid  13478  mgmlrid  13480  lidrideqd  13482  lidrididd  13483  grpinvalem  13486  grpinva  13487  gsum0g  13497  issgrp  13504  imasmnd2  13553  mnd1  13556  mnd1id  13557  idmhm  13570  issubm  13573  0mhm  13587  resmhm  13588  resmhm2  13589  resmhm2b  13590  dfgrp2  13628  isgrpid2  13641  grpidd2  13642  grpinvval  13644  grpressid  13662  grpsubid1  13686  dfgrp3mlem  13699  grplactfval  13702  imasgrp2  13715  mhmlem  13719  mulgfvalg  13726  mulgnnp1  13735  mulgsubcl  13741  mulgnncl  13742  mulgnn0cl  13743  mulgcl  13744  mulgnn0z  13754  mulgneg2  13761  mulgmodid  13766  submmulg  13771  issubg  13778  subgid  13780  subgex  13781  subg0  13785  subginv  13786  subgcl  13789  subgsub  13791  subgmulg  13793  issubg3  13797  isnsg  13807  isnsg3  13812  nmzsubg  13815  nmznsg  13818  eqgval  13828  idghm  13864  resghm  13865  ghmnsgima  13873  ablressid  13940  mgpvalg  13955  rngressid  13986  ringressid  14095  imasring  14096  opprvalg  14101  opprsubgg  14116  dvdsrex  14131  dvdsrtr  14134  unitinvcl  14156  unitinvinv  14157  unitlinv  14159  unitrinv  14160  issubrng  14232  subrngid  14234  issubrng2  14243  issubrg  14254  subrgid  14256  issubrg2  14274  rrgval  14295  isdomn  14302  lmodlema  14325  islmodd  14326  rmodislmod  14384  lsssn0  14403  sraval  14470  sraring  14482  sralmod  14483  rlmvalg  14487  rlmbasg  14488  rlmplusgg  14489  rlm0g  14490  rlmsubg  14491  rlmmulrg  14492  rlmscabas  14493  rlmvscag  14494  rlmtopng  14495  rlmdsg  14496  rlmvnegg  14498  lidlss  14509  lidlssbas  14510  lidlbas  14511  crngridl  14563  zringinvg  14637  mulgrhm  14642  znval  14669  znf1o  14684  psrelbasfun  14710  mplvalcoe  14723  tsettps  14781  baspartn  14793  eltg  14795  en1top  14820  isopn3  14868  resttopon  14914  lmbr2  14957  cnptopresti  14981  cndis  14984  lmfpm  14986  lmcl  14988  lmff  14992  txswaphmeolem  15063  ispsmet  15066  psmet0  15070  xmetunirn  15101  bl2in  15146  metrest  15249  expcn  15312  cncfmptid  15340  negcncf  15348  negfcncf  15349  hovera  15390  hoverb  15391  limccl  15402  eldvap  15425  dvexp  15454  dvmptid  15459  dveflem  15469  dvef  15470  elply  15477  plypow  15487  dvply1  15508  logge0b  15633  logle1b  15635  logcxp  15640  fsumdvdsmul  15734  perfectlem2  15743  zabsle1  15747  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdirnn0  15795  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2dlem1  15809  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1b  15837  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgsoddprmlem2  15854  2lgsoddprmlem3d  15858  edgfndxid  15879  uhgr0e  15952  umgrislfupgrdom  16001  ausgrusgrien  16041  egrsubgr  16133  uhgrsubgrself  16136  uhgrspanop  16152  clwwlkext2edg  16292  clwwlknccat  16293  clwwlknonmpo  16298  iseupth  16317  bj-ex  16409  bdth  16477  bj-indind  16578  gfsum0  16734