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  5636  funopsn  5817  fvsng  5835  isose  5945  canth  5952  riota2f  5977  riotaeqimp  5979  acexmidlemab  5995  fvoveq1  6024  0neqopab  6049  ssoprab2  6060  caovcld  6159  caovcomd  6162  caovassd  6165  caovcand  6168  caovordid  6172  caovordd  6174  caovdid  6181  caovdird  6184  caovimo  6199  f1opw  6213  caofref  6243  caofinvl  6244  caofid0l  6245  caofid0r  6246  xpexgALT  6278  op1stg  6296  op2ndg  6297  releldm2  6331  elopabi  6341  dfmpo  6369  smoeq  6436  tfr1onlemaccex  6494  tfrcllemaccex  6507  rdgisucinc  6531  rdg0g  6534  oacl  6606  nna0r  6624  nnmsucr  6634  ercnv  6701  swoord1  6709  swoord2  6710  eqer  6712  ider  6713  iinerm  6754  brecop  6772  ixpssmapg  6875  elixpsn  6882  en1bg  6952  fundmeng  6960  rex2dom  6971  xpsneng  6981  mapen  7007  phplem3g  7017  php5  7019  php5dom  7024  findcard2d  7053  findcard2sd  7054  undifdc  7086  xpfi  7094  elfir  7140  fi0  7142  ordiso2  7202  ctssdclemr  7279  nnnninfeq2  7296  nninfisol  7300  ctssexmid  7317  nninfinfwlpo  7347  exmidaclem  7390  djuenun  7394  exmidapne  7446  cc1  7451  cc2lem  7452  mulidnq  7576  ltsonq  7585  halfnqq  7597  nqnq0pi  7625  nq02m  7652  cauappcvgprlemm  7832  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem2  7847  cauappcvgpr  7849  ltposr  7950  0idsr  7954  1idsr  7955  mappsrprg  7991  ax1rid  8064  ax0id  8065  axpre-ltirr  8069  mulrid  8143  1p1times  8280  cnegexlem3  8323  pncan1  8523  npcan1  8524  kcnktkm1cn  8529  apirr  8752  recexap  8800  eqneg  8879  subrecap  8986  lediv2a  9042  nn1m1nn  9128  2txmxeqx  9242  subhalfhalf  9346  add1p1  9361  sub1m1  9362  cnm2m1cnm3  9363  xp1d2m1eqxm1d2  9364  div4p1lem1div2  9365  nn0addcl  9404  nn0mulcl  9405  zadd2cl  9576  nn0ledivnn  9963  nltpnft  10010  ngtmnft  10013  xrrebnd  10015  xnegneg  10029  xnegid  10055  xaddid1  10058  fzss1  10259  fzssp1  10263  fzshftral  10304  0elfz  10314  nn0fz0  10315  elfz0add  10316  fz0tp  10318  elfzoelz  10343  fzoval  10344  fzoss2  10370  fzossrbm1  10371  fzouzsplit  10377  elfzo1  10391  fzonn0p1  10417  fzossfzop1  10418  fzoend  10428  fzosplitsn  10439  fvinim0ffz  10447  2tnp1ge0ge0  10521  fldiv4p1lem1div2  10525  frec2uzltd  10625  frec2uzrand  10627  uzenom  10647  frecfzennn  10648  seqeq1  10672  iseqf1olemkle  10719  iseqf1olemklt  10720  iseqf1olemqk  10729  seq3f1olemstep  10736  seq3f1olemp  10737  seq3f1oleml  10738  seqf1oglem2  10742  seq3id  10747  seq3id2  10748  ser0f  10756  m1expcl2  10783  sqoddm1div8  10915  mulsubdivbinom2ap  10933  faclbnd  10963  facubnd  10967  bcpasc  10988  hashcl  11003  omgadd  11024  snopiswrd  11081  elovmpowrd  11113  lswwrd  11118  ccatval1  11132  ccatsymb  11137  ccatass  11143  ccat1st1st  11172  swrdf  11187  pfxsuff1eqwrdeq  11231  ccatpfx  11233  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12  11265  swrdccatin2d  11276  reuccatpfxs1lem  11278  s3eq2  11309  reval  11360  imval  11361  crim  11369  replim  11370  rexuz3  11501  absval  11512  sqrt0  11515  resqrexlemp1rp  11517  resqrexlemfp1  11520  resqrex  11537  abs00  11575  leabs  11585  absimle  11595  cau3  11626  dfabsmax  11728  climshft  11815  fsum3  11898  fsumcnv  11948  fsumiun  11988  binom  11995  bcxmaslem1  11999  isumshft  12001  arisum  12009  arisum2  12010  trireciplem  12011  trirecip  12012  geo2sum2  12026  geo2lim  12027  prodf1f  12054  prod0  12096  fprodfac  12126  ege2le3  12182  ef4p  12205  efgt1p2  12206  efgt1p  12207  sinval  12213  cosval  12214  negdvdsb  12318  dvdsnegb  12319  dvdsssfz1  12363  dvds1  12364  3dvds  12375  even2n  12385  oddge22np1  12392  2tp1odd  12395  ltoddhalfle  12404  m1expo  12411  m1exp1  12412  flodddiv4  12447  bits0e  12460  bits0o  12461  bitsp1e  12463  bitsp1o  12464  bitsfzo  12466  bitsinv1lem  12472  bitsinv1  12473  gcdsupex  12478  gcdsupcl  12479  alginv  12569  algcvg  12570  algcvga  12573  algfx  12574  eucalgcvga  12580  lcmdvds  12601  pw2dvds  12688  oddpwdclemodd  12694  phimul  12748  eulerth  12755  pc2dvds  12853  pcz  12855  pcmpt  12866  pcmptdvds  12868  fldivp1  12871  oddprmdvds  12877  pockthg  12880  pockthi  12881  1arith  12890  zgz  12896  4sqlem19  12932  evenennn  12964  ennnfonelemp1  12977  ennnfonelemkh  12983  ennnfonelemnn0  12993  ssnnctlemct  13017  strslfv2  13076  strslfv  13077  basm  13094  ressvalsets  13097  ressbasid  13103  pwsval  13324  qusex  13358  xpsfeq  13378  intopsn  13400  mgmidmo  13405  ismgmid  13410  mgmlrid  13412  lidrideqd  13414  lidrididd  13415  grpinvalem  13418  grpinva  13419  gsum0g  13429  issgrp  13436  imasmnd2  13485  mnd1  13488  mnd1id  13489  idmhm  13502  issubm  13505  0mhm  13519  resmhm  13520  resmhm2  13521  resmhm2b  13522  dfgrp2  13560  isgrpid2  13573  grpidd2  13574  grpinvval  13576  grpressid  13594  grpsubid1  13618  dfgrp3mlem  13631  grplactfval  13634  imasgrp2  13647  mhmlem  13651  mulgfvalg  13658  mulgnnp1  13667  mulgsubcl  13673  mulgnncl  13674  mulgnn0cl  13675  mulgcl  13676  mulgnn0z  13686  mulgneg2  13693  mulgmodid  13698  submmulg  13703  issubg  13710  subgid  13712  subgex  13713  subg0  13717  subginv  13718  subgcl  13721  subgsub  13723  subgmulg  13725  issubg3  13729  isnsg  13739  isnsg3  13744  nmzsubg  13747  nmznsg  13750  eqgval  13760  idghm  13796  resghm  13797  ghmnsgima  13805  ablressid  13872  mgpvalg  13886  rngressid  13917  ringressid  14026  imasring  14027  opprvalg  14032  opprsubgg  14047  dvdsrex  14062  dvdsrtr  14065  unitinvcl  14087  unitinvinv  14088  unitlinv  14090  unitrinv  14091  issubrng  14163  subrngid  14165  issubrng2  14174  issubrg  14185  subrgid  14187  issubrg2  14205  rrgval  14226  isdomn  14233  lmodlema  14256  islmodd  14257  rmodislmod  14315  lsssn0  14334  sraval  14401  sraring  14413  sralmod  14414  rlmvalg  14418  rlmbasg  14419  rlmplusgg  14420  rlm0g  14421  rlmsubg  14422  rlmmulrg  14423  rlmscabas  14424  rlmvscag  14425  rlmtopng  14426  rlmdsg  14427  rlmvnegg  14429  lidlss  14440  lidlssbas  14441  lidlbas  14442  crngridl  14494  zringinvg  14568  mulgrhm  14573  znval  14600  znf1o  14615  psrelbasfun  14641  mplvalcoe  14654  tsettps  14712  baspartn  14724  eltg  14726  en1top  14751  isopn3  14799  resttopon  14845  lmbr2  14888  cnptopresti  14912  cndis  14915  lmfpm  14917  lmcl  14919  lmff  14923  txswaphmeolem  14994  ispsmet  14997  psmet0  15001  xmetunirn  15032  bl2in  15077  metrest  15180  expcn  15243  cncfmptid  15271  negcncf  15279  negfcncf  15280  hovera  15321  hoverb  15322  limccl  15333  eldvap  15356  dvexp  15385  dvmptid  15390  dveflem  15400  dvef  15401  elply  15408  plypow  15418  dvply1  15439  logge0b  15564  logle1b  15566  logcxp  15571  fsumdvdsmul  15665  perfectlem2  15674  zabsle1  15678  lgsval  15683  lgsfvalg  15684  lgsval2lem  15689  lgsdir2lem2  15708  lgsdir2lem4  15710  lgsdirnn0  15726  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2dlem1  15740  2lgslem1a1  15765  2lgslem1a2  15766  2lgslem1b  15768  2lgslem1c  15769  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgsoddprmlem2  15785  2lgsoddprmlem3d  15789  edgfndxid  15810  uhgr0e  15882  umgrislfupgrdom  15929  ausgrusgrien  15969  bj-ex  16126  bdth  16194  bj-indind  16295