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  529  simprl  531  simprr  533  pm3.45  601  pm5.36  614  con2i  632  notnot  634  con3i  637  biijust  646  con3  647  con2  648  pm5.19  714  olc  719  orc  720  pm2.621  755  pm1.2  764  orim1i  768  orim2i  769  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  orim2  797  orbi1  800  pm2.38  811  pm2.74  815  pm3.2ni  821  biort  837  dcbiit  847  pm4.79dc  911  dcand  941  biantr  961  3anim1i  1212  3anim2i  1213  3anim3i  1214  mpd3an23  1376  trujust  1400  tru  1402  dftru2  1406  truimtru  1454  falimfal  1457  3impexp  1483  19.26  1530  19.8a  1639  19.9ht  1690  hbn  1699  19.36i  1720  19.41h  1733  equsb1  1834  sbieh  1839  dveeq2or  1865  spsbim  1892  2ax17  1927  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  moanmo  2160  nfcvf  2409  neqne  2422  neneq  2436  necon3i  2462  nebidc  2494  r19.27v  2672  r19.28v  2673  vtoclgft  2867  rspcime  2931  eueq2dc  2993  cdeqcv  3039  ru  3044  sbcied2  3083  sbcralt  3122  sbcrext  3123  csbiebt  3181  csbied2  3189  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  ssid  3262  difss2  3351  ddifstab  3355  abvor0dc  3536  ssdifeq0  3596  rabsnt  3771  unisng  3936  dfnfc2  3937  ssbr  4158  a9evsep  4237  axnul  4240  rabex2  4263  intid  4345  opm  4355  opth1  4357  opth  4358  copsex4g  4368  0nelop  4369  moop2  4373  pocl  4429  swopo  4432  limeq  4503  suceq  4528  eusvnfb  4580  onintexmid  4700  nn0eln0  4747  elvvuni  4819  coss1  4915  coss2  4916  dmxpm  4982  elrnmpt1  5013  soirri  5162  relcnvtr  5287  relssdmrn  5288  cnvpom  5310  fveqeq2  5684  fsn2g  5857  funopsn  5865  fvsng  5885  isose  6000  canth  6009  riota2f  6034  riotaeqimp  6036  acexmidlemab  6052  fvoveq1  6081  0neqopab  6106  ssoprab2  6117  caovcld  6216  caovcomd  6219  caovassd  6222  caovcand  6225  caovordid  6229  caovordd  6231  caovdid  6238  caovdird  6241  caovimo  6256  f1opw  6270  caofref  6300  caofinvl  6301  caofid0l  6302  caofid0r  6303  xpexgALT  6339  op1stg  6357  op2ndg  6358  releldm2  6392  opabn1stprc  6402  elopabi  6404  dfmpo  6432  smoeq  6534  tfr1onlemaccex  6592  tfrcllemaccex  6605  rdgisucinc  6629  rdg0g  6632  oacl  6706  nna0r  6724  nnmsucr  6734  ercnv  6801  swoord1  6809  swoord2  6810  eqer  6812  ider  6813  iinerm  6854  brecop  6872  ixpssmapg  6976  elixpsn  6983  en1bg  7053  fundmeng  7061  rex2dom  7076  xpsneng  7086  mapen  7112  phplem3g  7123  php5  7125  php5dom  7130  findcard2d  7161  findcard2sd  7162  undifdc  7197  xpfi  7205  fsuppxpfi  7262  elfir  7273  fi0  7275  ordiso2  7339  ctssdclemr  7416  nnnninfeq2  7433  nninfisol  7437  ctssexmid  7454  nninfinfwlpo  7484  exmidaclem  7528  djuenun  7532  papeq2  7574  papirr  7575  exmidapne  7590  cc1  7595  cc2lem  7596  mulidnq  7720  ltsonq  7729  halfnqq  7741  nqnq0pi  7769  nq02m  7796  cauappcvgprlemm  7976  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  cauappcvgpr  7993  ltposr  8094  0idsr  8098  1idsr  8099  mappsrprg  8135  ax1rid  8208  ax0id  8209  axpre-ltirr  8213  mulrid  8287  1p1times  8423  cnegexlem3  8466  pncan1  8667  npcan1  8668  kcnktkm1cn  8673  apirr  8896  recexap  8944  eqneg  9023  subrecap  9130  lediv2a  9186  nn1m1nn  9272  2txmxeqx  9386  subhalfhalf  9490  add1p1  9505  sub1m1  9506  cnm2m1cnm3  9507  xp1d2m1eqxm1d2  9508  div4p1lem1div2  9509  nn0addcl  9548  nn0mulcl  9549  zadd2cl  9725  nn0ledivnn  10118  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xnegneg  10185  xnegid  10211  xaddid1  10214  fzss1  10418  fzssp1  10422  fzshftral  10464  0elfz  10474  nn0fz0  10475  elfz0add  10476  fz0tp  10478  elfzoelz  10503  fzoval  10504  fzoss2  10530  fzossrbm1  10531  fzouzsplit  10537  elfzo1  10552  fzonn0p1  10578  fzossfzop1  10579  fzoend  10589  fzosplitsn  10600  fvinim0ffz  10609  2tnp1ge0ge0  10685  fldiv4p1lem1div2  10689  frec2uzltd  10789  frec2uzrand  10791  uzenom  10811  frecfzennn  10812  seqeq1  10836  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqk  10893  seq3f1olemstep  10900  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem2  10906  seq3id  10911  seq3id2  10912  ser0f  10920  m1expcl2  10947  resq01  11044  sqoddm1div8  11080  mulsubdivbinom2ap  11098  faclbnd  11128  facubnd  11132  bcpasc  11153  hashcl  11169  omgadd  11191  hashfibc  11232  snopiswrd  11259  elovmpowrd  11291  lswwrd  11296  ccatval1  11310  ccatsymb  11315  ccatass  11321  ccat1st1st  11354  swrdf  11372  pfxsuff1eqwrdeq  11416  ccatpfx  11418  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccatin2d  11461  reuccatpfxs1lem  11463  s3eq2  11494  reval  11559  imval  11560  crim  11568  replim  11569  rexuz3  11700  absval  11711  sqrt0  11714  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrex  11736  abs00  11774  leabs  11784  absimle  11794  cau3  11825  dfabsmax  11927  climshft  12014  fsum3  12098  fsumcnv  12148  fsumiun  12188  binom  12195  bcxmaslem1  12199  isumshft  12201  arisum  12209  arisum2  12210  trireciplem  12211  trirecip  12212  geo2sum2  12226  geo2lim  12227  prodf1f  12254  prod0  12296  fprodfac  12326  ege2le3  12382  ef4p  12405  efgt1p2  12406  efgt1p  12407  sinval  12413  cosval  12414  negdvdsb  12518  dvdsnegb  12519  dvdsssfz1  12563  dvds1  12564  3dvds  12575  even2n  12585  oddge22np1  12592  2tp1odd  12595  ltoddhalfle  12604  m1expo  12611  m1exp1  12612  flodddiv4  12647  bits0e  12660  bits0o  12661  bitsp1e  12663  bitsp1o  12664  bitsfzo  12666  bitsinv1lem  12672  bitsinv1  12673  gcdsupex  12678  gcdsupcl  12679  alginv  12769  algcvg  12770  algcvga  12773  algfx  12774  eucalgcvga  12780  lcmdvds  12801  pw2dvds  12888  oddpwdclemodd  12894  phimul  12948  eulerth  12955  pc2dvds  13053  pcz  13055  pcmpt  13066  pcmptdvds  13068  fldivp1  13071  oddprmdvds  13077  pockthg  13080  pockthi  13081  1arith  13090  zgz  13096  4sqlem19  13132  ballotfilemfmpn  13178  ballotfilemfval0  13179  ballotfilemsv  13197  ballotfilemsf1o  13201  ballotfilemrval  13205  ballotfilemro  13210  ballotfilemrinv  13221  ballotfi  13226  evenennn  13228  ennnfonelemp1  13241  ennnfonelemkh  13247  ennnfonelemnn0  13257  ssnnctlemct  13281  strslfv2  13340  strslfv  13341  basm  13358  ressvalsets  13361  ressbasid  13367  qusex  13589  xpsfeq  13609  intopsn  13630  mgmidmo  13635  ismgmid  13640  mgmlrid  13642  lidrideqd  13644  lidrididd  13645  grpinvalem  13648  grpinva  13649  gsum0g  13659  issgrp  13666  imasmnd2  13707  mnd1  13710  mnd1id  13711  idmhm  13724  issubm  13727  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  dfgrp2  13782  isgrpid2  13795  grpidd2  13796  grpinvval  13798  grpressid  13816  grpsubid1  13840  dfgrp3mlem  13853  grplactfval  13856  imasgrp2  13863  mhmlem  13867  mulgfvalg  13874  mulgnnp1  13883  mulgsubcl  13889  mulgnncl  13890  mulgnn0cl  13891  mulgcl  13892  mulgnn0z  13902  mulgneg2  13909  mulgmodid  13914  submmulg  13919  issubg  13926  subgid  13928  subgex  13929  subg0  13933  subginv  13934  subgcl  13937  subgsub  13939  subgmulg  13941  issubg3  13945  isnsg  13955  isnsg3  13960  nmzsubg  13963  nmznsg  13966  eqgval  13976  idghm  14012  resghm  14013  ghmnsgima  14021  ablressid  14088  gfsum0  14104  pwsval  14146  mgpvalg  14162  rngressid  14193  ringressid  14306  imasring  14307  opprvalg  14312  opprsubgg  14328  dvdsrex  14343  dvdsrtr  14346  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  opprlring  14442  issubrng  14445  subrngid  14447  issubrng2  14456  issubrg  14467  subrgid  14469  issubrg2  14487  rrgval  14508  isdomn  14516  aprprop  14539  drnggrp  14551  opprdrng  14558  lmodlema  14566  islmodd  14567  rmodislmod  14625  lsssn0  14644  sraval  14711  sraring  14723  sralmod  14724  rlmvalg  14728  rlmbasg  14729  rlmplusgg  14730  rlm0g  14731  rlmsubg  14732  rlmmulrg  14733  rlmscabas  14734  rlmvscag  14735  rlmtopng  14736  rlmdsg  14737  rlmvnegg  14739  lidlss  14750  lidlssbas  14751  lidlbas  14752  crngridl  14804  zringinvg  14878  mulgrhm  14883  znval  14910  znf1o  14925  psrbagfsupp  14945  psrbaglesupp  14948  psrbaglecl  14950  psrbagcon  14952  psrelbasfun  14958  mplvalcoe  14971  tsettps  15029  baspartn  15041  eltg  15043  en1top  15068  isopn3  15116  resttopon  15162  lmbr2  15205  cnptopresti  15229  cndis  15232  lmfpm  15234  lmcl  15236  lmff  15240  txswaphmeolem  15311  ispsmet  15314  psmet0  15318  xmetunirn  15349  bl2in  15394  metrest  15497  expcn  15560  cncfmptid  15588  negcncf  15596  negfcncf  15597  hovera  15638  hoverb  15639  limccl  15650  eldvap  15673  dvexp  15702  dvmptid  15707  dveflem  15717  dvef  15718  elply  15725  plypow  15735  dvply1  15756  logge0b  15881  logle1b  15883  logcxp  15888  fsumdvdsmul  15985  perfectlem2  15994  zabsle1  15998  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdirnn0  16046  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  gausslemma2dlem1  16060  2lgslem1a1  16085  2lgslem1a2  16086  2lgslem1b  16088  2lgslem1c  16089  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgsoddprmlem2  16105  2lgsoddprmlem3d  16109  edgfndxid  16130  uhgr0e  16203  umgrislfupgrdom  16252  ausgrusgrien  16292  egrsubgr  16384  uhgrsubgrself  16387  uhgrspanop  16403  clwwlkext2edg  16543  clwwlknccat  16544  clwwlknonmpo  16549  iseupth  16568  bj-ex  16660  bdth  16727  bj-indind  16828  exmidcon  16906  exmidpeirce  16907