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  101  biimprd  158  biimpcd  159  biimprcd  160  biid  171  bibi2i  227  imbi1  236  imbi2  237  bibi1  240  pm3.3  261  pm3.31  262  jctl  314  jctr  315  ancli  323  ancri  324  anc2li  329  anc2ri  330  anim12i  338  anim1i  340  anim1ci  341  anim2i  342  pm4.24  395  anass  401  mpdan  421  mpancom  422  pm5.32  453  anbi1  466  anbi2  467  mpan10  474  adantl3r  512  simpll  527  simplr  528  simprl  529  simprr  531  pm3.45  599  pm5.36  612  con2i  630  notnot  632  con3i  635  biijust  644  con3  645  con2  646  pm5.19  711  olc  716  orc  717  pm2.621  752  pm1.2  761  orim1i  765  orim2i  766  pm2.41  781  pm2.42  782  pm2.4  783  pm4.44  784  orim2  794  orbi1  797  pm2.38  808  pm2.74  812  pm3.2ni  818  biort  834  dcbiit  844  pm4.79dc  908  dcand  938  biantr  958  3anim1i  1209  3anim2i  1210  3anim3i  1211  mpd3an23  1373  trujust  1397  tru  1399  dftru2  1403  truimtru  1451  falimfal  1454  3impexp  1480  19.26  1527  19.8a  1636  19.9ht  1687  ax6blem  1696  19.36i  1718  19.41h  1731  equsb1  1831  sbieh  1836  dveeq2or  1862  spsbim  1889  2ax17  1924  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  moanmo  2155  nfcvf  2395  neqne  2408  neneq  2422  necon3i  2448  nebidc  2480  r19.27v  2658  r19.28v  2659  vtoclgft  2851  rspcime  2914  eueq2dc  2976  cdeqcv  3022  ru  3027  sbcied2  3066  sbcralt  3105  sbcrext  3106  csbiebt  3164  csbied2  3172  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ssid  3244  difss2  3332  ddifstab  3336  abvor0dc  3515  ssdifeq0  3574  rabsnt  3741  unisng  3904  dfnfc2  3905  ssbr  4126  a9evsep  4205  axnul  4208  rabex2  4229  intid  4309  opm  4319  opth1  4321  opth  4322  copsex4g  4332  0nelop  4333  moop2  4337  pocl  4393  swopo  4396  limeq  4467  suceq  4492  eusvnfb  4544  onintexmid  4664  nn0eln0  4711  elvvuni  4782  coss1  4876  coss2  4877  dmxpm  4943  elrnmpt1  4974  soirri  5122  relcnvtr  5247  relssdmrn  5248  cnvpom  5270  fveqeq2  5635  funopsn  5816  fvsng  5834  isose  5944  canth  5951  riota2f  5976  riotaeqimp  5978  acexmidlemab  5994  fvoveq1  6023  0neqopab  6048  ssoprab2  6059  caovcld  6158  caovcomd  6161  caovassd  6164  caovcand  6167  caovordid  6171  caovordd  6173  caovdid  6180  caovdird  6183  caovimo  6198  f1opw  6211  caofref  6241  caofinvl  6242  caofid0l  6243  caofid0r  6244  xpexgALT  6276  op1stg  6294  op2ndg  6295  releldm2  6329  elopabi  6339  dfmpo  6367  smoeq  6434  tfr1onlemaccex  6492  tfrcllemaccex  6505  rdgisucinc  6529  rdg0g  6532  oacl  6604  nna0r  6622  nnmsucr  6632  ercnv  6699  swoord1  6707  swoord2  6708  eqer  6710  ider  6711  iinerm  6752  brecop  6770  ixpssmapg  6873  elixpsn  6880  en1bg  6950  fundmeng  6958  rex2dom  6969  xpsneng  6977  mapen  7003  phplem3g  7013  php5  7015  php5dom  7020  findcard2d  7049  findcard2sd  7050  undifdc  7082  xpfi  7090  elfir  7136  fi0  7138  ordiso2  7198  ctssdclemr  7275  nnnninfeq2  7292  nninfisol  7296  ctssexmid  7313  nninfinfwlpo  7343  exmidaclem  7386  djuenun  7390  exmidapne  7442  cc1  7447  cc2lem  7448  mulidnq  7572  ltsonq  7581  halfnqq  7593  nqnq0pi  7621  nq02m  7648  cauappcvgprlemm  7828  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem2  7843  cauappcvgpr  7845  ltposr  7946  0idsr  7950  1idsr  7951  mappsrprg  7987  ax1rid  8060  ax0id  8061  axpre-ltirr  8065  mulrid  8139  1p1times  8276  cnegexlem3  8319  pncan1  8519  npcan1  8520  kcnktkm1cn  8525  apirr  8748  recexap  8796  eqneg  8875  subrecap  8982  lediv2a  9038  nn1m1nn  9124  2txmxeqx  9238  subhalfhalf  9342  add1p1  9357  sub1m1  9358  cnm2m1cnm3  9359  xp1d2m1eqxm1d2  9360  div4p1lem1div2  9361  nn0addcl  9400  nn0mulcl  9401  zadd2cl  9572  nn0ledivnn  9959  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xnegneg  10025  xnegid  10051  xaddid1  10054  fzss1  10255  fzssp1  10259  fzshftral  10300  0elfz  10310  nn0fz0  10311  elfz0add  10312  fz0tp  10314  elfzoelz  10339  fzoval  10340  fzoss2  10366  fzossrbm1  10367  fzouzsplit  10373  elfzo1  10386  fzonn0p1  10412  fzossfzop1  10413  fzoend  10423  fzosplitsn  10434  fvinim0ffz  10442  2tnp1ge0ge0  10516  fldiv4p1lem1div2  10520  frec2uzltd  10620  frec2uzrand  10622  uzenom  10642  frecfzennn  10643  seqeq1  10667  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqk  10724  seq3f1olemstep  10731  seq3f1olemp  10732  seq3f1oleml  10733  seqf1oglem2  10737  seq3id  10742  seq3id2  10743  ser0f  10751  m1expcl2  10778  sqoddm1div8  10910  mulsubdivbinom2ap  10928  faclbnd  10958  facubnd  10962  bcpasc  10983  hashcl  10998  omgadd  11019  snopiswrd  11076  elovmpowrd  11108  lswwrd  11113  ccatval1  11127  ccatsymb  11132  ccatass  11138  ccat1st1st  11167  swrdf  11182  pfxsuff1eqwrdeq  11226  ccatpfx  11228  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccatin2d  11271  reuccatpfxs1lem  11273  s3eq2  11304  reval  11355  imval  11356  crim  11364  replim  11365  rexuz3  11496  absval  11507  sqrt0  11510  resqrexlemp1rp  11512  resqrexlemfp1  11515  resqrex  11532  abs00  11570  leabs  11580  absimle  11590  cau3  11621  dfabsmax  11723  climshft  11810  fsum3  11893  fsumcnv  11943  fsumiun  11983  binom  11990  bcxmaslem1  11994  isumshft  11996  arisum  12004  arisum2  12005  trireciplem  12006  trirecip  12007  geo2sum2  12021  geo2lim  12022  prodf1f  12049  prod0  12091  fprodfac  12121  ege2le3  12177  ef4p  12200  efgt1p2  12201  efgt1p  12202  sinval  12208  cosval  12209  negdvdsb  12313  dvdsnegb  12314  dvdsssfz1  12358  dvds1  12359  3dvds  12370  even2n  12380  oddge22np1  12387  2tp1odd  12390  ltoddhalfle  12399  m1expo  12406  m1exp1  12407  flodddiv4  12442  bits0e  12455  bits0o  12456  bitsp1e  12458  bitsp1o  12459  bitsfzo  12461  bitsinv1lem  12467  bitsinv1  12468  gcdsupex  12473  gcdsupcl  12474  alginv  12564  algcvg  12565  algcvga  12568  algfx  12569  eucalgcvga  12575  lcmdvds  12596  pw2dvds  12683  oddpwdclemodd  12689  phimul  12743  eulerth  12750  pc2dvds  12848  pcz  12850  pcmpt  12861  pcmptdvds  12863  fldivp1  12866  oddprmdvds  12872  pockthg  12875  pockthi  12876  1arith  12885  zgz  12891  4sqlem19  12927  evenennn  12959  ennnfonelemp1  12972  ennnfonelemkh  12978  ennnfonelemnn0  12988  ssnnctlemct  13012  strslfv2  13071  strslfv  13072  basm  13089  ressvalsets  13092  ressbasid  13098  pwsval  13319  qusex  13353  xpsfeq  13373  intopsn  13395  mgmidmo  13400  ismgmid  13405  mgmlrid  13407  lidrideqd  13409  lidrididd  13410  grpinvalem  13413  grpinva  13414  gsum0g  13424  issgrp  13431  imasmnd2  13480  mnd1  13483  mnd1id  13484  idmhm  13497  issubm  13500  0mhm  13514  resmhm  13515  resmhm2  13516  resmhm2b  13517  dfgrp2  13555  isgrpid2  13568  grpidd2  13569  grpinvval  13571  grpressid  13589  grpsubid1  13613  dfgrp3mlem  13626  grplactfval  13629  imasgrp2  13642  mhmlem  13646  mulgfvalg  13653  mulgnnp1  13662  mulgsubcl  13668  mulgnncl  13669  mulgnn0cl  13670  mulgcl  13671  mulgnn0z  13681  mulgneg2  13688  mulgmodid  13693  submmulg  13698  issubg  13705  subgid  13707  subgex  13708  subg0  13712  subginv  13713  subgcl  13716  subgsub  13718  subgmulg  13720  issubg3  13724  isnsg  13734  isnsg3  13739  nmzsubg  13742  nmznsg  13745  eqgval  13755  idghm  13791  resghm  13792  ghmnsgima  13800  ablressid  13867  mgpvalg  13881  rngressid  13912  ringressid  14021  imasring  14022  opprvalg  14027  opprsubgg  14042  dvdsrex  14056  dvdsrtr  14059  unitinvcl  14081  unitinvinv  14082  unitlinv  14084  unitrinv  14085  issubrng  14157  subrngid  14159  issubrng2  14168  issubrg  14179  subrgid  14181  issubrg2  14199  rrgval  14220  isdomn  14227  lmodlema  14250  islmodd  14251  rmodislmod  14309  lsssn0  14328  sraval  14395  sraring  14407  sralmod  14408  rlmvalg  14412  rlmbasg  14413  rlmplusgg  14414  rlm0g  14415  rlmsubg  14416  rlmmulrg  14417  rlmscabas  14418  rlmvscag  14419  rlmtopng  14420  rlmdsg  14421  rlmvnegg  14423  lidlss  14434  lidlssbas  14435  lidlbas  14436  crngridl  14488  zringinvg  14562  mulgrhm  14567  znval  14594  znf1o  14609  psrelbasfun  14635  mplvalcoe  14648  tsettps  14706  baspartn  14718  eltg  14720  en1top  14745  isopn3  14793  resttopon  14839  lmbr2  14882  cnptopresti  14906  cndis  14909  lmfpm  14911  lmcl  14913  lmff  14917  txswaphmeolem  14988  ispsmet  14991  psmet0  14995  xmetunirn  15026  bl2in  15071  metrest  15174  expcn  15237  cncfmptid  15265  negcncf  15273  negfcncf  15274  hovera  15315  hoverb  15316  limccl  15327  eldvap  15350  dvexp  15379  dvmptid  15384  dveflem  15394  dvef  15395  elply  15402  plypow  15412  dvply1  15433  logge0b  15558  logle1b  15560  logcxp  15565  fsumdvdsmul  15659  perfectlem2  15668  zabsle1  15672  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdirnn0  15720  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  gausslemma2dlem1  15734  2lgslem1a1  15759  2lgslem1a2  15760  2lgslem1b  15762  2lgslem1c  15763  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem2  15779  2lgsoddprmlem3d  15783  edgfndxid  15804  uhgr0e  15876  umgrislfupgrdom  15923  ausgrusgrien  15963  bj-ex  16084  bdth  16152  bj-indind  16253