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  anim1ci  339  anim2i  340  pm4.24  393  anass  399  mpdan  418  mpancom  419  pm5.32  449  anbi1  462  anbi2  463  mpan10  466  adantl3r  504  simpll  519  simplr  520  simprl  521  simprr  522  pm3.45  587  pm5.36  600  con2i  617  notnot  619  con3i  622  biijust  631  con3  632  con2  633  pm5.19  696  olc  701  orc  702  pm2.621  737  pm1.2  746  orim1i  750  orim2i  751  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  orim2  779  orbi1  782  pm2.38  793  pm2.74  797  pm3.2ni  803  dcbiit  825  pm4.79dc  889  biantr  937  3anim1i  1168  3anim2i  1169  3anim3i  1170  mpd3an23  1318  trujust  1334  tru  1336  dftru2  1340  truimtru  1388  falimfal  1391  3impexp  1414  19.26  1458  19.8a  1570  19.9ht  1621  ax6blem  1629  19.36i  1651  19.41h  1664  equsb1  1759  sbieh  1764  dveeq2or  1789  spsbim  1816  2ax17  1851  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  moanmo  2077  nfcvf  2304  neqne  2317  neneq  2331  necon3i  2357  nebidc  2389  r19.27v  2562  r19.28v  2563  vtoclgft  2739  rspcime  2800  eueq2dc  2861  cdeqcv  2907  ru  2912  sbcied2  2950  sbcralt  2989  sbcrext  2990  csbiebt  3044  csbied2  3052  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  ssid  3122  difss2  3209  ddifstab  3213  abvor0dc  3391  ssdifeq0  3450  rabsnt  3606  unisng  3761  dfnfc2  3762  a9evsep  4058  axnul  4061  intid  4154  opm  4164  opth1  4166  opth  4167  copsex4g  4177  0nelop  4178  moop2  4181  pocl  4233  swopo  4236  limeq  4307  suceq  4332  eusvnfb  4383  onintexmid  4495  nn0eln0  4541  elvvuni  4611  coss1  4702  coss2  4703  dmxpm  4767  elrnmpt1  4798  soirri  4941  relcnvtr  5066  relssdmrn  5067  cnvpom  5089  fveqeq2  5438  fvsng  5624  isose  5730  riota2f  5759  acexmidlemab  5776  fvoveq1  5805  0neqopab  5824  ssoprab2  5835  caovcld  5932  caovcomd  5935  caovassd  5938  caovcand  5941  caovordid  5945  caovordd  5947  caovdid  5954  caovdird  5957  caovimo  5972  grprinvlem  5973  grprinvd  5974  f1opw  5985  caofref  6011  caofinvl  6012  xpexgALT  6039  op1stg  6056  op2ndg  6057  releldm2  6091  elopabi  6101  dfmpo  6128  smoeq  6195  tfr1onlemaccex  6253  tfrcllemaccex  6266  rdgisucinc  6290  rdg0g  6293  oacl  6364  nna0r  6382  nnmsucr  6392  ercnv  6458  swoord1  6466  swoord2  6467  eqer  6469  ider  6470  iinerm  6509  brecop  6527  ixpssmapg  6630  elixpsn  6637  en1bg  6702  fundmeng  6709  xpsneng  6724  mapen  6748  phplem3g  6758  php5  6760  php5dom  6765  findcard2d  6793  findcard2sd  6794  undifdc  6820  xpfi  6826  elfir  6869  fi0  6871  ordiso2  6928  ctssdclemr  7005  ctssexmid  7032  exmidaclem  7081  djuenun  7085  cc1  7097  cc2lem  7098  mulidnq  7221  ltsonq  7230  halfnqq  7242  nqnq0pi  7270  nq02m  7297  cauappcvgprlemm  7477  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem2  7492  cauappcvgpr  7494  ltposr  7595  0idsr  7599  1idsr  7600  mappsrprg  7636  ax1rid  7709  ax0id  7710  axpre-ltirr  7714  mulid1  7787  1p1times  7920  cnegexlem3  7963  pncan1  8163  npcan1  8164  kcnktkm1cn  8169  apirr  8391  recexap  8438  eqneg  8516  subrecap  8622  lediv2a  8677  nn1m1nn  8762  add1p1  8993  sub1m1  8994  cnm2m1cnm3  8995  xp1d2m1eqxm1d2  8996  div4p1lem1div2  8997  nn0addcl  9036  nn0mulcl  9037  zadd2cl  9204  nn0ledivnn  9584  nltpnft  9627  ngtmnft  9630  xrrebnd  9632  xnegneg  9646  xnegid  9672  xaddid1  9675  fzss1  9874  fzssp1  9878  fzshftral  9919  0elfz  9929  nn0fz0  9930  elfz0add  9931  fz0tp  9932  elfzoelz  9955  fzoval  9956  fzoss2  9980  fzossrbm1  9981  fzouzsplit  9987  elfzo1  9998  fzonn0p1  10019  fzossfzop1  10020  fzoend  10030  fzosplitsn  10041  fvinim0ffz  10049  2tnp1ge0ge0  10105  fldiv4p1lem1div2  10109  frec2uzltd  10207  frec2uzrand  10209  uzenom  10229  frecfzennn  10230  seqeq1  10252  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemqk  10298  seq3f1olemstep  10305  seq3f1olemp  10306  seq3f1oleml  10307  seq3id  10312  seq3id2  10313  ser0f  10319  m1expcl2  10346  sqoddm1div8  10475  faclbnd  10519  facubnd  10523  bcpasc  10544  hashcl  10559  omgadd  10580  reval  10653  imval  10654  crim  10662  replim  10663  rexuz3  10794  absval  10805  sqrt0  10808  resqrexlemp1rp  10810  resqrexlemfp1  10813  resqrex  10830  abs00  10868  leabs  10878  absimle  10888  cau3  10919  dfabsmax  11021  climshft  11105  fsum3  11188  fsumcnv  11238  fsumiun  11278  binom  11285  bcxmaslem1  11289  isumshft  11291  arisum  11299  arisum2  11300  trireciplem  11301  trirecip  11302  geo2sum2  11316  geo2lim  11317  prodf1f  11344  ege2le3  11414  ef4p  11437  efgt1p2  11438  efgt1p  11439  sinval  11445  cosval  11446  negdvdsb  11545  dvdsnegb  11546  dvdsssfz1  11586  dvds1  11587  even2n  11607  oddge22np1  11614  2tp1odd  11617  ltoddhalfle  11626  m1expo  11633  m1exp1  11634  flodddiv4  11667  gcdsupex  11682  gcdsupcl  11683  alginv  11764  algcvg  11765  algcvga  11768  algfx  11769  eucalgcvga  11775  lcmdvds  11796  pw2dvds  11880  oddpwdclemodd  11886  phimul  11938  evenennn  11942  ennnfonelemp1  11955  ennnfonelemkh  11961  ennnfonelemnn0  11971  strslfv2  12041  strslfv  12042  ressid  12059  tsettps  12244  baspartn  12256  eltg  12260  en1top  12285  isopn3  12333  resttopon  12379  lmbr2  12422  cnptopresti  12446  cndis  12449  lmfpm  12451  lmcl  12453  lmff  12457  txswaphmeolem  12528  ispsmet  12531  psmet0  12535  xmetunirn  12566  bl2in  12611  metrest  12714  cncfmptid  12791  negcncf  12796  negfcncf  12797  limccl  12836  eldvap  12859  dvexp  12883  dveflem  12895  dvef  12896  logge0b  13019  logle1b  13021  logcxp  13026  bj-ex  13140  bdth  13200  bj-indind  13301