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  100  biimprd  157  biimpcd  158  biimprcd  159  biid  170  bibi2i  226  imbi1  235  imbi2  236  bibi1  239  pm3.3  259  pm3.31  260  jctl  312  jctr  313  ancli  321  ancri  322  anc2li  327  anc2ri  328  anim12i  336  anim1i  338  anim2i  339  pm4.24  392  anass  398  mpdan  417  mpancom  418  pm5.32  448  anbi1  461  anbi2  462  mpan10  465  adantl3r  503  simpll  518  simplr  519  simprl  520  simprr  521  pm3.45  586  pm5.36  599  con2i  616  notnot  618  con3i  621  biijust  630  con3  631  con2  632  pm5.19  695  olc  700  orc  701  pm2.621  736  pm1.2  745  orim1i  749  orim2i  750  pm2.41  765  pm2.42  766  pm2.4  767  pm4.44  768  orim2  778  orbi1  781  pm2.38  792  pm2.74  796  pm3.2ni  802  dcbiit  824  pm4.79dc  888  biantr  936  3anim1i  1167  3anim2i  1168  3anim3i  1169  mpd3an23  1317  trujust  1333  tru  1335  dftru2  1339  truimtru  1387  falimfal  1390  3impexp  1413  19.26  1457  19.8a  1569  19.9ht  1620  ax6blem  1628  19.36i  1650  19.41h  1663  equsb1  1758  sbieh  1763  dveeq2or  1788  spsbim  1815  2ax17  1850  dvelimALT  1983  dvelimfv  1984  dvelimor  1991  moanmo  2074  nfcvf  2301  neqne  2314  neneq  2328  necon3i  2354  nebidc  2386  r19.27v  2557  r19.28v  2558  vtoclgft  2731  rspcime  2791  eueq2dc  2852  cdeqcv  2898  ru  2903  sbcied2  2941  sbcralt  2980  sbcrext  2981  csbiebt  3034  csbied2  3042  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  ssid  3112  difss2  3199  ddifstab  3203  abvor0dc  3381  ssdifeq0  3440  rabsnt  3593  unisng  3748  dfnfc2  3749  a9evsep  4045  axnul  4048  intid  4141  opm  4151  opth1  4153  opth  4154  copsex4g  4164  0nelop  4165  moop2  4168  pocl  4220  swopo  4223  limeq  4294  suceq  4319  eusvnfb  4370  onintexmid  4482  nn0eln0  4528  elvvuni  4598  coss1  4689  coss2  4690  dmxpm  4754  elrnmpt1  4785  soirri  4928  relcnvtr  5053  relssdmrn  5054  cnvpom  5076  fveqeq2  5423  fvsng  5609  isose  5715  riota2f  5744  acexmidlemab  5761  fvoveq1  5790  0neqopab  5809  ssoprab2  5820  caovcld  5917  caovcomd  5920  caovassd  5923  caovcand  5926  caovordid  5930  caovordd  5932  caovdid  5939  caovdird  5942  caovimo  5957  grprinvlem  5958  grprinvd  5959  f1opw  5970  caofref  5996  caofinvl  5997  xpexgALT  6024  op1stg  6041  op2ndg  6042  releldm2  6076  elopabi  6086  dfmpo  6113  smoeq  6180  tfr1onlemaccex  6238  tfrcllemaccex  6251  rdgisucinc  6275  rdg0g  6278  oacl  6349  nna0r  6367  nnmsucr  6377  ercnv  6443  swoord1  6451  swoord2  6452  eqer  6454  ider  6455  iinerm  6494  brecop  6512  ixpssmapg  6615  elixpsn  6622  en1bg  6687  fundmeng  6694  xpsneng  6709  mapen  6733  phplem3g  6743  php5  6745  php5dom  6750  findcard2d  6778  findcard2sd  6779  undifdc  6805  xpfi  6811  elfir  6854  fi0  6856  ordiso2  6913  ctssdclemr  6990  ctssexmid  7017  exmidaclem  7057  djuenun  7061  mulidnq  7190  ltsonq  7199  halfnqq  7211  nqnq0pi  7239  nq02m  7266  cauappcvgprlemm  7446  cauappcvgprlemloc  7453  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem2  7461  cauappcvgpr  7463  ltposr  7564  0idsr  7568  1idsr  7569  mappsrprg  7605  ax1rid  7678  ax0id  7679  axpre-ltirr  7683  mulid1  7756  1p1times  7889  cnegexlem3  7932  pncan1  8132  npcan1  8133  kcnktkm1cn  8138  apirr  8360  recexap  8407  eqneg  8485  subrecap  8591  lediv2a  8646  nn1m1nn  8731  add1p1  8962  sub1m1  8963  cnm2m1cnm3  8964  xp1d2m1eqxm1d2  8965  div4p1lem1div2  8966  nn0addcl  9005  nn0mulcl  9006  zadd2cl  9173  nn0ledivnn  9547  nltpnft  9590  ngtmnft  9593  xrrebnd  9595  xnegneg  9609  xnegid  9635  xaddid1  9638  fzss1  9836  fzssp1  9840  fzshftral  9881  0elfz  9891  nn0fz0  9892  elfz0add  9893  fz0tp  9894  elfzoelz  9917  fzoval  9918  fzoss2  9942  fzossrbm1  9943  fzouzsplit  9949  elfzo1  9960  fzonn0p1  9981  fzossfzop1  9982  fzoend  9992  fzosplitsn  10003  fvinim0ffz  10011  2tnp1ge0ge0  10067  fldiv4p1lem1div2  10071  frec2uzltd  10169  frec2uzrand  10171  uzenom  10191  frecfzennn  10192  seqeq1  10214  iseqf1olemkle  10250  iseqf1olemklt  10251  iseqf1olemqk  10260  seq3f1olemstep  10267  seq3f1olemp  10268  seq3f1oleml  10269  seq3id  10274  seq3id2  10275  ser0f  10281  m1expcl2  10308  sqoddm1div8  10437  faclbnd  10480  facubnd  10484  bcpasc  10505  hashcl  10520  omgadd  10541  reval  10614  imval  10615  crim  10623  replim  10624  rexuz3  10755  absval  10766  sqrt0  10769  resqrexlemp1rp  10771  resqrexlemfp1  10774  resqrex  10791  abs00  10829  leabs  10839  absimle  10849  cau3  10880  dfabsmax  10982  climshft  11066  fsum3  11149  fsumcnv  11199  fsumiun  11239  binom  11246  bcxmaslem1  11250  isumshft  11252  arisum  11260  arisum2  11261  trireciplem  11262  trirecip  11263  geo2sum2  11277  geo2lim  11278  prodf1f  11305  ege2le3  11366  ef4p  11389  efgt1p2  11390  efgt1p  11391  sinval  11398  cosval  11399  negdvdsb  11498  dvdsnegb  11499  dvdsssfz1  11539  dvds1  11540  even2n  11560  oddge22np1  11567  2tp1odd  11570  ltoddhalfle  11579  m1expo  11586  m1exp1  11587  flodddiv4  11620  gcdsupex  11635  gcdsupcl  11636  alginv  11717  algcvg  11718  algcvga  11721  algfx  11722  eucalgcvga  11728  lcmdvds  11749  pw2dvds  11833  oddpwdclemodd  11839  phimul  11891  evenennn  11895  ennnfonelemp1  11908  ennnfonelemkh  11914  ennnfonelemnn0  11924  strslfv2  11991  strslfv  11992  ressid  12009  tsettps  12194  baspartn  12206  eltg  12210  en1top  12235  isopn3  12283  resttopon  12329  lmbr2  12372  cnptopresti  12396  cndis  12399  lmfpm  12401  lmcl  12403  lmff  12407  txswaphmeolem  12478  ispsmet  12481  psmet0  12485  xmetunirn  12516  bl2in  12561  metrest  12664  cncfmptid  12741  negcncf  12746  negfcncf  12747  limccl  12786  eldvap  12809  dvexp  12833  dveflem  12844  dvef  12845  bj-ex  12958  bdth  13018  bj-indind  13119