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  419  mpancom  420  pm5.32  450  anbi1  463  anbi2  464  mpan10  471  adantl3r  509  simpll  524  simplr  525  simprl  526  simprr  527  pm3.45  592  pm5.36  605  con2i  622  notnot  624  con3i  627  biijust  636  con3  637  con2  638  pm5.19  701  olc  706  orc  707  pm2.621  742  pm1.2  751  orim1i  755  orim2i  756  pm2.41  771  pm2.42  772  pm2.4  773  pm4.44  774  orim2  784  orbi1  787  pm2.38  798  pm2.74  802  pm3.2ni  808  biort  824  dcbiit  834  pm4.79dc  898  biantr  947  3anim1i  1180  3anim2i  1181  3anim3i  1182  mpd3an23  1334  trujust  1350  tru  1352  dftru2  1356  truimtru  1404  falimfal  1407  3impexp  1430  19.26  1474  19.8a  1583  19.9ht  1634  ax6blem  1643  19.36i  1665  19.41h  1678  equsb1  1778  sbieh  1783  dveeq2or  1809  spsbim  1836  2ax17  1871  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  moanmo  2096  nfcvf  2335  neqne  2348  neneq  2362  necon3i  2388  nebidc  2420  r19.27v  2597  r19.28v  2598  vtoclgft  2780  rspcime  2841  eueq2dc  2903  cdeqcv  2949  ru  2954  sbcied2  2992  sbcralt  3031  sbcrext  3032  csbiebt  3088  csbied2  3096  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  ssid  3167  difss2  3255  ddifstab  3259  abvor0dc  3438  ssdifeq0  3497  rabsnt  3658  unisng  3813  dfnfc2  3814  a9evsep  4111  axnul  4114  intid  4209  opm  4219  opth1  4221  opth  4222  copsex4g  4232  0nelop  4233  moop2  4236  pocl  4288  swopo  4291  limeq  4362  suceq  4387  eusvnfb  4439  onintexmid  4557  nn0eln0  4604  elvvuni  4675  coss1  4766  coss2  4767  dmxpm  4831  elrnmpt1  4862  soirri  5005  relcnvtr  5130  relssdmrn  5131  cnvpom  5153  fveqeq2  5505  fvsng  5692  isose  5800  canth  5807  riota2f  5830  acexmidlemab  5847  fvoveq1  5876  0neqopab  5898  ssoprab2  5909  caovcld  6006  caovcomd  6009  caovassd  6012  caovcand  6015  caovordid  6019  caovordd  6021  caovdid  6028  caovdird  6031  caovimo  6046  f1opw  6056  caofref  6082  caofinvl  6083  xpexgALT  6112  op1stg  6129  op2ndg  6130  releldm2  6164  elopabi  6174  dfmpo  6202  smoeq  6269  tfr1onlemaccex  6327  tfrcllemaccex  6340  rdgisucinc  6364  rdg0g  6367  oacl  6439  nna0r  6457  nnmsucr  6467  ercnv  6534  swoord1  6542  swoord2  6543  eqer  6545  ider  6546  iinerm  6585  brecop  6603  ixpssmapg  6706  elixpsn  6713  en1bg  6778  fundmeng  6785  xpsneng  6800  mapen  6824  phplem3g  6834  php5  6836  php5dom  6841  findcard2d  6869  findcard2sd  6870  undifdc  6901  xpfi  6907  elfir  6950  fi0  6952  ordiso2  7012  ctssdclemr  7089  nnnninfeq2  7105  nninfisol  7109  ctssexmid  7126  exmidaclem  7185  djuenun  7189  cc1  7227  cc2lem  7228  mulidnq  7351  ltsonq  7360  halfnqq  7372  nqnq0pi  7400  nq02m  7427  cauappcvgprlemm  7607  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem2  7622  cauappcvgpr  7624  ltposr  7725  0idsr  7729  1idsr  7730  mappsrprg  7766  ax1rid  7839  ax0id  7840  axpre-ltirr  7844  mulid1  7917  1p1times  8053  cnegexlem3  8096  pncan1  8296  npcan1  8297  kcnktkm1cn  8302  apirr  8524  recexap  8571  eqneg  8649  subrecap  8756  lediv2a  8811  nn1m1nn  8896  add1p1  9127  sub1m1  9128  cnm2m1cnm3  9129  xp1d2m1eqxm1d2  9130  div4p1lem1div2  9131  nn0addcl  9170  nn0mulcl  9171  zadd2cl  9341  nn0ledivnn  9724  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xnegneg  9790  xnegid  9816  xaddid1  9819  fzss1  10019  fzssp1  10023  fzshftral  10064  0elfz  10074  nn0fz0  10075  elfz0add  10076  fz0tp  10078  elfzoelz  10103  fzoval  10104  fzoss2  10128  fzossrbm1  10129  fzouzsplit  10135  elfzo1  10146  fzonn0p1  10167  fzossfzop1  10168  fzoend  10178  fzosplitsn  10189  fvinim0ffz  10197  2tnp1ge0ge0  10257  fldiv4p1lem1div2  10261  frec2uzltd  10359  frec2uzrand  10361  uzenom  10381  frecfzennn  10382  seqeq1  10404  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqk  10450  seq3f1olemstep  10457  seq3f1olemp  10458  seq3f1oleml  10459  seq3id  10464  seq3id2  10465  ser0f  10471  m1expcl2  10498  sqoddm1div8  10629  faclbnd  10675  facubnd  10679  bcpasc  10700  hashcl  10715  omgadd  10737  reval  10813  imval  10814  crim  10822  replim  10823  rexuz3  10954  absval  10965  sqrt0  10968  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrex  10990  abs00  11028  leabs  11038  absimle  11048  cau3  11079  dfabsmax  11181  climshft  11267  fsum3  11350  fsumcnv  11400  fsumiun  11440  binom  11447  bcxmaslem1  11451  isumshft  11453  arisum  11461  arisum2  11462  trireciplem  11463  trirecip  11464  geo2sum2  11478  geo2lim  11479  prodf1f  11506  prod0  11548  fprodfac  11578  ege2le3  11634  ef4p  11657  efgt1p2  11658  efgt1p  11659  sinval  11665  cosval  11666  negdvdsb  11769  dvdsnegb  11770  dvdsssfz1  11812  dvds1  11813  even2n  11833  oddge22np1  11840  2tp1odd  11843  ltoddhalfle  11852  m1expo  11859  m1exp1  11860  flodddiv4  11893  gcdsupex  11912  gcdsupcl  11913  alginv  12001  algcvg  12002  algcvga  12005  algfx  12006  eucalgcvga  12012  lcmdvds  12033  pw2dvds  12120  oddpwdclemodd  12126  phimul  12180  eulerth  12187  pc2dvds  12283  pcz  12285  pcmpt  12295  pcmptdvds  12297  fldivp1  12300  oddprmdvds  12306  pockthg  12309  pockthi  12310  1arith  12319  zgz  12325  evenennn  12348  ennnfonelemp1  12361  ennnfonelemkh  12367  ennnfonelemnn0  12377  ssnnctlemct  12401  strslfv2  12459  strslfv  12460  ressid  12479  intopsn  12621  mgmidmo  12626  ismgmid  12631  mgmlrid  12633  lidrideqd  12635  lidrididd  12636  grprinvlem  12639  grprinvd  12640  issgrp  12644  mnd1  12679  mnd1id  12680  idmhm  12692  issubm  12695  0mhm  12704  dfgrp2  12732  isgrpid2  12743  grpidd2  12744  grpinvval  12746  tsettps  12830  baspartn  12842  eltg  12846  en1top  12871  isopn3  12919  resttopon  12965  lmbr2  13008  cnptopresti  13032  cndis  13035  lmfpm  13037  lmcl  13039  lmff  13043  txswaphmeolem  13114  ispsmet  13117  psmet0  13121  xmetunirn  13152  bl2in  13197  metrest  13300  cncfmptid  13377  negcncf  13382  negfcncf  13383  limccl  13422  eldvap  13445  dvexp  13469  dveflem  13481  dvef  13482  logge0b  13605  logle1b  13607  logcxp  13612  zabsle1  13694  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdirnn0  13742  bj-ex  13797  bdth  13866  bj-indind  13967