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  707  olc  712  orc  713  pm2.621  748  pm1.2  757  orim1i  761  orim2i  762  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  orim2  790  orbi1  793  pm2.38  804  pm2.74  808  pm3.2ni  814  biort  830  dcbiit  840  pm4.79dc  904  dcand  934  biantr  954  3anim1i  1187  3anim2i  1188  3anim3i  1189  mpd3an23  1350  trujust  1366  tru  1368  dftru2  1372  truimtru  1420  falimfal  1423  3impexp  1448  19.26  1492  19.8a  1601  19.9ht  1652  ax6blem  1661  19.36i  1683  19.41h  1696  equsb1  1796  sbieh  1801  dveeq2or  1827  spsbim  1854  2ax17  1889  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  moanmo  2119  nfcvf  2359  neqne  2372  neneq  2386  necon3i  2412  nebidc  2444  r19.27v  2621  r19.28v  2622  vtoclgft  2810  rspcime  2871  eueq2dc  2933  cdeqcv  2979  ru  2984  sbcied2  3023  sbcralt  3062  sbcrext  3063  csbiebt  3120  csbied2  3128  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  ssid  3199  difss2  3287  ddifstab  3291  abvor0dc  3470  ssdifeq0  3529  rabsnt  3693  unisng  3852  dfnfc2  3853  a9evsep  4151  axnul  4154  rabex2  4175  intid  4253  opm  4263  opth1  4265  opth  4266  copsex4g  4276  0nelop  4277  moop2  4280  pocl  4334  swopo  4337  limeq  4408  suceq  4433  eusvnfb  4485  onintexmid  4605  nn0eln0  4652  elvvuni  4723  coss1  4817  coss2  4818  dmxpm  4882  elrnmpt1  4913  soirri  5060  relcnvtr  5185  relssdmrn  5186  cnvpom  5208  fveqeq2  5563  fvsng  5754  isose  5864  canth  5871  riota2f  5895  acexmidlemab  5912  fvoveq1  5941  0neqopab  5963  ssoprab2  5974  caovcld  6072  caovcomd  6075  caovassd  6078  caovcand  6081  caovordid  6085  caovordd  6087  caovdid  6094  caovdird  6097  caovimo  6112  f1opw  6125  caofref  6154  caofinvl  6155  xpexgALT  6185  op1stg  6203  op2ndg  6204  releldm2  6238  elopabi  6248  dfmpo  6276  smoeq  6343  tfr1onlemaccex  6401  tfrcllemaccex  6414  rdgisucinc  6438  rdg0g  6441  oacl  6513  nna0r  6531  nnmsucr  6541  ercnv  6608  swoord1  6616  swoord2  6617  eqer  6619  ider  6620  iinerm  6661  brecop  6679  ixpssmapg  6782  elixpsn  6789  en1bg  6854  fundmeng  6861  xpsneng  6876  mapen  6902  phplem3g  6912  php5  6914  php5dom  6919  findcard2d  6947  findcard2sd  6948  undifdc  6980  xpfi  6986  elfir  7032  fi0  7034  ordiso2  7094  ctssdclemr  7171  nnnninfeq2  7188  nninfisol  7192  ctssexmid  7209  exmidaclem  7268  djuenun  7272  exmidapne  7320  cc1  7325  cc2lem  7326  mulidnq  7449  ltsonq  7458  halfnqq  7470  nqnq0pi  7498  nq02m  7525  cauappcvgprlemm  7705  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem2  7720  cauappcvgpr  7722  ltposr  7823  0idsr  7827  1idsr  7828  mappsrprg  7864  ax1rid  7937  ax0id  7938  axpre-ltirr  7942  mulrid  8016  1p1times  8153  cnegexlem3  8196  pncan1  8396  npcan1  8397  kcnktkm1cn  8402  apirr  8624  recexap  8672  eqneg  8751  subrecap  8858  lediv2a  8914  nn1m1nn  9000  subhalfhalf  9217  add1p1  9232  sub1m1  9233  cnm2m1cnm3  9234  xp1d2m1eqxm1d2  9235  div4p1lem1div2  9236  nn0addcl  9275  nn0mulcl  9276  zadd2cl  9446  nn0ledivnn  9833  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xnegneg  9899  xnegid  9925  xaddid1  9928  fzss1  10129  fzssp1  10133  fzshftral  10174  0elfz  10184  nn0fz0  10185  elfz0add  10186  fz0tp  10188  elfzoelz  10213  fzoval  10214  fzoss2  10239  fzossrbm1  10240  fzouzsplit  10246  elfzo1  10257  fzonn0p1  10278  fzossfzop1  10279  fzoend  10289  fzosplitsn  10300  fvinim0ffz  10308  2tnp1ge0ge0  10370  fldiv4p1lem1div2  10374  frec2uzltd  10474  frec2uzrand  10476  uzenom  10496  frecfzennn  10497  seqeq1  10521  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqk  10578  seq3f1olemstep  10585  seq3f1olemp  10586  seq3f1oleml  10587  seqf1oglem2  10591  seq3id  10596  seq3id2  10597  ser0f  10605  m1expcl2  10632  sqoddm1div8  10764  mulsubdivbinom2ap  10782  faclbnd  10812  facubnd  10816  bcpasc  10837  hashcl  10852  omgadd  10873  snopiswrd  10924  elovmpowrd  10955  reval  10993  imval  10994  crim  11002  replim  11003  rexuz3  11134  absval  11145  sqrt0  11148  resqrexlemp1rp  11150  resqrexlemfp1  11153  resqrex  11170  abs00  11208  leabs  11218  absimle  11228  cau3  11259  dfabsmax  11361  climshft  11447  fsum3  11530  fsumcnv  11580  fsumiun  11620  binom  11627  bcxmaslem1  11631  isumshft  11633  arisum  11641  arisum2  11642  trireciplem  11643  trirecip  11644  geo2sum2  11658  geo2lim  11659  prodf1f  11686  prod0  11728  fprodfac  11758  ege2le3  11814  ef4p  11837  efgt1p2  11838  efgt1p  11839  sinval  11845  cosval  11846  negdvdsb  11950  dvdsnegb  11951  dvdsssfz1  11994  dvds1  11995  even2n  12015  oddge22np1  12022  2tp1odd  12025  ltoddhalfle  12034  m1expo  12041  m1exp1  12042  flodddiv4  12075  gcdsupex  12094  gcdsupcl  12095  alginv  12185  algcvg  12186  algcvga  12189  algfx  12190  eucalgcvga  12196  lcmdvds  12217  pw2dvds  12304  oddpwdclemodd  12310  phimul  12364  eulerth  12371  pc2dvds  12468  pcz  12470  pcmpt  12481  pcmptdvds  12483  fldivp1  12486  oddprmdvds  12492  pockthg  12495  pockthi  12496  1arith  12505  zgz  12511  4sqlem19  12547  evenennn  12550  ennnfonelemp1  12563  ennnfonelemkh  12569  ennnfonelemnn0  12579  ssnnctlemct  12603  strslfv2  12662  strslfv  12663  basm  12679  ressvalsets  12682  ressbasid  12688  qusex  12908  xpsfeq  12928  intopsn  12950  mgmidmo  12955  ismgmid  12960  mgmlrid  12962  lidrideqd  12964  lidrididd  12965  grpinvalem  12968  grpinva  12969  gsum0g  12979  issgrp  12986  mnd1  13027  mnd1id  13028  idmhm  13041  issubm  13044  0mhm  13058  resmhm  13059  resmhm2  13060  resmhm2b  13061  dfgrp2  13099  isgrpid2  13112  grpidd2  13113  grpinvval  13115  grpressid  13133  grpsubid1  13157  dfgrp3mlem  13170  grplactfval  13173  imasgrp2  13180  mhmlem  13184  mulgfvalg  13191  mulgnnp1  13200  mulgsubcl  13206  mulgnncl  13207  mulgnn0cl  13208  mulgcl  13209  mulgnn0z  13219  mulgneg2  13226  mulgmodid  13231  submmulg  13236  issubg  13243  subgid  13245  subgex  13246  subg0  13250  subginv  13251  subgcl  13254  subgsub  13256  subgmulg  13258  issubg3  13262  isnsg  13272  isnsg3  13277  nmzsubg  13280  nmznsg  13283  eqgval  13293  idghm  13329  resghm  13330  ghmnsgima  13338  ablressid  13405  mgpvalg  13419  rngressid  13450  ringressid  13559  imasring  13560  opprvalg  13565  opprsubgg  13580  dvdsrex  13594  dvdsrtr  13597  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  issubrng  13695  subrngid  13697  issubrng2  13706  issubrg  13717  subrgid  13719  issubrg2  13737  rrgval  13758  isdomn  13765  lmodlema  13788  islmodd  13789  rmodislmod  13847  lsssn0  13866  sraval  13933  sraring  13945  sralmod  13946  rlmvalg  13950  rlmbasg  13951  rlmplusgg  13952  rlm0g  13953  rlmsubg  13954  rlmmulrg  13955  rlmscabas  13956  rlmvscag  13957  rlmtopng  13958  rlmdsg  13959  rlmvnegg  13961  lidlss  13972  lidlssbas  13973  lidlbas  13974  crngridl  14026  zringinvg  14092  mulgrhm  14097  znval  14124  znf1o  14139  psrelbasfun  14161  tsettps  14206  baspartn  14218  eltg  14220  en1top  14245  isopn3  14293  resttopon  14339  lmbr2  14382  cnptopresti  14406  cndis  14409  lmfpm  14411  lmcl  14413  lmff  14417  txswaphmeolem  14488  ispsmet  14491  psmet0  14495  xmetunirn  14526  bl2in  14571  metrest  14674  cncfmptid  14751  negcncf  14759  negfcncf  14760  hovera  14801  hoverb  14802  limccl  14813  eldvap  14836  dvexp  14860  dveflem  14872  dvef  14873  elply  14880  plypow  14890  logge0b  15025  logle1b  15027  logcxp  15032  zabsle1  15115  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdirnn0  15163  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2dlem1  15177  2lgsoddprmlem2  15194  2lgsoddprmlem3d  15198  bj-ex  15254  bdth  15323  bj-indind  15424