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	⊢ (𝜑 → 𝜑)

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (𝜑 → 𝜑))
2		ax-1 6	. 2 ⊢ (𝜑 → ((𝜑 → 𝜑) → 𝜑))
3	1, 2	mpd 13	1 ⊢ (𝜑 → 𝜑)

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  biort  819  dcbiit  829  pm4.79dc  893  biantr  941  3anim1i  1174  3anim2i  1175  3anim3i  1176  mpd3an23  1328  trujust  1344  tru  1346  dftru2  1350  truimtru  1398  falimfal  1401  3impexp  1424  19.26  1468  19.8a  1577  19.9ht  1628  ax6blem  1637  19.36i  1659  19.41h  1672  equsb1  1772  sbieh  1777  dveeq2or  1803  spsbim  1830  2ax17  1865  dvelimALT  1997  dvelimfv  1998  dvelimor  2005  moanmo  2090  nfcvf  2329  neqne  2342  neneq  2356  necon3i  2382  nebidc  2414  r19.27v  2591  r19.28v  2592  vtoclgft  2771  rspcime  2832  eueq2dc  2894  cdeqcv  2940  ru  2945  sbcied2  2983  sbcralt  3022  sbcrext  3023  csbiebt  3079  csbied2  3087  cbvralcsf  3102  cbvrexcsf  3103  cbvreucsf  3104  cbvrabcsf  3105  ssid  3157  difss2  3245  ddifstab  3249  abvor0dc  3427  ssdifeq0  3486  rabsnt  3645  unisng  3800  dfnfc2  3801  a9evsep  4098  axnul  4101  intid  4196  opm  4206  opth1  4208  opth  4209  copsex4g  4219  0nelop  4220  moop2  4223  pocl  4275  swopo  4278  limeq  4349  suceq  4374  eusvnfb  4426  onintexmid  4544  nn0eln0  4591  elvvuni  4662  coss1  4753  coss2  4754  dmxpm  4818  elrnmpt1  4849  soirri  4992  relcnvtr  5117  relssdmrn  5118  cnvpom  5140  fveqeq2  5489  fvsng  5675  isose  5783  canth  5790  riota2f  5813  acexmidlemab  5830  fvoveq1  5859  0neqopab  5878  ssoprab2  5889  caovcld  5986  caovcomd  5989  caovassd  5992  caovcand  5995  caovordid  5999  caovordd  6001  caovdid  6008  caovdird  6011  caovimo  6026  grprinvlem  6027  grprinvd  6028  f1opw  6039  caofref  6065  caofinvl  6066  xpexgALT  6093  op1stg  6110  op2ndg  6111  releldm2  6145  elopabi  6155  dfmpo  6182  smoeq  6249  tfr1onlemaccex  6307  tfrcllemaccex  6320  rdgisucinc  6344  rdg0g  6347  oacl  6419  nna0r  6437  nnmsucr  6447  ercnv  6513  swoord1  6521  swoord2  6522  eqer  6524  ider  6525  iinerm  6564  brecop  6582  ixpssmapg  6685  elixpsn  6692  en1bg  6757  fundmeng  6764  xpsneng  6779  mapen  6803  phplem3g  6813  php5  6815  php5dom  6820  findcard2d  6848  findcard2sd  6849  undifdc  6880  xpfi  6886  elfir  6929  fi0  6931  ordiso2  6991  ctssdclemr  7068  nnnninfeq2  7084  nninfisol  7088  ctssexmid  7105  exmidaclem  7155  djuenun  7159  cc1  7197  cc2lem  7198  mulidnq  7321  ltsonq  7330  halfnqq  7342  nqnq0pi  7370  nq02m  7397  cauappcvgprlemm  7577  cauappcvgprlemloc  7584  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem2  7592  cauappcvgpr  7594  ltposr  7695  0idsr  7699  1idsr  7700  mappsrprg  7736  ax1rid  7809  ax0id  7810  axpre-ltirr  7814  mulid1  7887  1p1times  8023  cnegexlem3  8066  pncan1  8266  npcan1  8267  kcnktkm1cn  8272  apirr  8494  recexap  8541  eqneg  8619  subrecap  8726  lediv2a  8781  nn1m1nn  8866  add1p1  9097  sub1m1  9098  cnm2m1cnm3  9099  xp1d2m1eqxm1d2  9100  div4p1lem1div2  9101  nn0addcl  9140  nn0mulcl  9141  zadd2cl  9311  nn0ledivnn  9694  nltpnft  9741  ngtmnft  9744  xrrebnd  9746  xnegneg  9760  xnegid  9786  xaddid1  9789  fzss1  9988  fzssp1  9992  fzshftral  10033  0elfz  10043  nn0fz0  10044  elfz0add  10045  fz0tp  10047  elfzoelz  10072  fzoval  10073  fzoss2  10097  fzossrbm1  10098  fzouzsplit  10104  elfzo1  10115  fzonn0p1  10136  fzossfzop1  10137  fzoend  10147  fzosplitsn  10158  fvinim0ffz  10166  2tnp1ge0ge0  10226  fldiv4p1lem1div2  10230  frec2uzltd  10328  frec2uzrand  10330  uzenom  10350  frecfzennn  10351  seqeq1  10373  iseqf1olemkle  10409  iseqf1olemklt  10410  iseqf1olemqk  10419  seq3f1olemstep  10426  seq3f1olemp  10427  seq3f1oleml  10428  seq3id  10433  seq3id2  10434  ser0f  10440  m1expcl2  10467  sqoddm1div8  10597  faclbnd  10643  facubnd  10647  bcpasc  10668  hashcl  10683  omgadd  10704  reval  10777  imval  10778  crim  10786  replim  10787  rexuz3  10918  absval  10929  sqrt0  10932  resqrexlemp1rp  10934  resqrexlemfp1  10937  resqrex  10954  abs00  10992  leabs  11002  absimle  11012  cau3  11043  dfabsmax  11145  climshft  11231  fsum3  11314  fsumcnv  11364  fsumiun  11404  binom  11411  bcxmaslem1  11415  isumshft  11417  arisum  11425  arisum2  11426  trireciplem  11427  trirecip  11428  geo2sum2  11442  geo2lim  11443  prodf1f  11470  prod0  11512  fprodfac  11542  ege2le3  11598  ef4p  11621  efgt1p2  11622  efgt1p  11623  sinval  11629  cosval  11630  negdvdsb  11733  dvdsnegb  11734  dvdsssfz1  11775  dvds1  11776  even2n  11796  oddge22np1  11803  2tp1odd  11806  ltoddhalfle  11815  m1expo  11822  m1exp1  11823  flodddiv4  11856  gcdsupex  11875  gcdsupcl  11876  alginv  11958  algcvg  11959  algcvga  11962  algfx  11963  eucalgcvga  11969  lcmdvds  11990  pw2dvds  12075  oddpwdclemodd  12081  phimul  12135  eulerth  12142  pc2dvds  12238  pcz  12240  pcmpt  12250  pcmptdvds  12252  fldivp1  12255  oddprmdvds  12261  evenennn  12263  ennnfonelemp1  12276  ennnfonelemkh  12282  ennnfonelemnn0  12292  ssnnctlemct  12316  strslfv2  12374  strslfv  12375  ressid  12392  tsettps  12577  baspartn  12589  eltg  12593  en1top  12618  isopn3  12666  resttopon  12712  lmbr2  12755  cnptopresti  12779  cndis  12782  lmfpm  12784  lmcl  12786  lmff  12790  txswaphmeolem  12861  ispsmet  12864  psmet0  12868  xmetunirn  12899  bl2in  12944  metrest  13047  cncfmptid  13124  negcncf  13129  negfcncf  13130  limccl  13169  eldvap  13192  dvexp  13216  dveflem  13228  dvef  13229  logge0b  13352  logle1b  13354  logcxp  13359  bj-ex  13478  bdth  13548  bj-indind  13649