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  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  1985  dvelimfv  1986  dvelimor  1993  moanmo  2076  nfcvf  2303  neqne  2316  neneq  2330  necon3i  2356  nebidc  2388  r19.27v  2559  r19.28v  2560  vtoclgft  2736  rspcime  2796  eueq2dc  2857  cdeqcv  2903  ru  2908  sbcied2  2946  sbcralt  2985  sbcrext  2986  csbiebt  3039  csbied2  3047  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  ssid  3117  difss2  3204  ddifstab  3208  abvor0dc  3386  ssdifeq0  3445  rabsnt  3598  unisng  3753  dfnfc2  3754  a9evsep  4050  axnul  4053  intid  4146  opm  4156  opth1  4158  opth  4159  copsex4g  4169  0nelop  4170  moop2  4173  pocl  4225  swopo  4228  limeq  4299  suceq  4324  eusvnfb  4375  onintexmid  4487  nn0eln0  4533  elvvuni  4603  coss1  4694  coss2  4695  dmxpm  4759  elrnmpt1  4790  soirri  4933  relcnvtr  5058  relssdmrn  5059  cnvpom  5081  fveqeq2  5430  fvsng  5616  isose  5722  riota2f  5751  acexmidlemab  5768  fvoveq1  5797  0neqopab  5816  ssoprab2  5827  caovcld  5924  caovcomd  5927  caovassd  5930  caovcand  5933  caovordid  5937  caovordd  5939  caovdid  5946  caovdird  5949  caovimo  5964  grprinvlem  5965  grprinvd  5966  f1opw  5977  caofref  6003  caofinvl  6004  xpexgALT  6031  op1stg  6048  op2ndg  6049  releldm2  6083  elopabi  6093  dfmpo  6120  smoeq  6187  tfr1onlemaccex  6245  tfrcllemaccex  6258  rdgisucinc  6282  rdg0g  6285  oacl  6356  nna0r  6374  nnmsucr  6384  ercnv  6450  swoord1  6458  swoord2  6459  eqer  6461  ider  6462  iinerm  6501  brecop  6519  ixpssmapg  6622  elixpsn  6629  en1bg  6694  fundmeng  6701  xpsneng  6716  mapen  6740  phplem3g  6750  php5  6752  php5dom  6757  findcard2d  6785  findcard2sd  6786  undifdc  6812  xpfi  6818  elfir  6861  fi0  6863  ordiso2  6920  ctssdclemr  6997  ctssexmid  7024  exmidaclem  7064  djuenun  7068  mulidnq  7197  ltsonq  7206  halfnqq  7218  nqnq0pi  7246  nq02m  7273  cauappcvgprlemm  7453  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem2  7468  cauappcvgpr  7470  ltposr  7571  0idsr  7575  1idsr  7576  mappsrprg  7612  ax1rid  7685  ax0id  7686  axpre-ltirr  7690  mulid1  7763  1p1times  7896  cnegexlem3  7939  pncan1  8139  npcan1  8140  kcnktkm1cn  8145  apirr  8367  recexap  8414  eqneg  8492  subrecap  8598  lediv2a  8653  nn1m1nn  8738  add1p1  8969  sub1m1  8970  cnm2m1cnm3  8971  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  nn0addcl  9012  nn0mulcl  9013  zadd2cl  9180  nn0ledivnn  9554  nltpnft  9597  ngtmnft  9600  xrrebnd  9602  xnegneg  9616  xnegid  9642  xaddid1  9645  fzss1  9843  fzssp1  9847  fzshftral  9888  0elfz  9898  nn0fz0  9899  elfz0add  9900  fz0tp  9901  elfzoelz  9924  fzoval  9925  fzoss2  9949  fzossrbm1  9950  fzouzsplit  9956  elfzo1  9967  fzonn0p1  9988  fzossfzop1  9989  fzoend  9999  fzosplitsn  10010  fvinim0ffz  10018  2tnp1ge0ge0  10074  fldiv4p1lem1div2  10078  frec2uzltd  10176  frec2uzrand  10178  uzenom  10198  frecfzennn  10199  seqeq1  10221  iseqf1olemkle  10257  iseqf1olemklt  10258  iseqf1olemqk  10267  seq3f1olemstep  10274  seq3f1olemp  10275  seq3f1oleml  10276  seq3id  10281  seq3id2  10282  ser0f  10288  m1expcl2  10315  sqoddm1div8  10444  faclbnd  10487  facubnd  10491  bcpasc  10512  hashcl  10527  omgadd  10548  reval  10621  imval  10622  crim  10630  replim  10631  rexuz3  10762  absval  10773  sqrt0  10776  resqrexlemp1rp  10778  resqrexlemfp1  10781  resqrex  10798  abs00  10836  leabs  10846  absimle  10856  cau3  10887  dfabsmax  10989  climshft  11073  fsum3  11156  fsumcnv  11206  fsumiun  11246  binom  11253  bcxmaslem1  11257  isumshft  11259  arisum  11267  arisum2  11268  trireciplem  11269  trirecip  11270  geo2sum2  11284  geo2lim  11285  prodf1f  11312  ege2le3  11377  ef4p  11400  efgt1p2  11401  efgt1p  11402  sinval  11409  cosval  11410  negdvdsb  11509  dvdsnegb  11510  dvdsssfz1  11550  dvds1  11551  even2n  11571  oddge22np1  11578  2tp1odd  11581  ltoddhalfle  11590  m1expo  11597  m1exp1  11598  flodddiv4  11631  gcdsupex  11646  gcdsupcl  11647  alginv  11728  algcvg  11729  algcvga  11732  algfx  11733  eucalgcvga  11739  lcmdvds  11760  pw2dvds  11844  oddpwdclemodd  11850  phimul  11902  evenennn  11906  ennnfonelemp1  11919  ennnfonelemkh  11925  ennnfonelemnn0  11935  strslfv2  12002  strslfv  12003  ressid  12020  tsettps  12205  baspartn  12217  eltg  12221  en1top  12246  isopn3  12294  resttopon  12340  lmbr2  12383  cnptopresti  12407  cndis  12410  lmfpm  12412  lmcl  12414  lmff  12418  txswaphmeolem  12489  ispsmet  12492  psmet0  12496  xmetunirn  12527  bl2in  12572  metrest  12675  cncfmptid  12752  negcncf  12757  negfcncf  12758  limccl  12797  eldvap  12820  dvexp  12844  dveflem  12855  dvef  12856  bj-ex  12969  bdth  13029  bj-indind  13130