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  713  olc  718  orc  719  pm2.621  754  pm1.2  763  orim1i  767  orim2i  768  pm2.41  783  pm2.42  784  pm2.4  785  pm4.44  786  orim2  796  orbi1  799  pm2.38  810  pm2.74  814  pm3.2ni  820  biort  836  dcbiit  846  pm4.79dc  910  dcand  940  biantr  960  3anim1i  1211  3anim2i  1212  3anim3i  1213  mpd3an23  1375  trujust  1399  tru  1401  dftru2  1405  truimtru  1453  falimfal  1456  3impexp  1482  19.26  1529  19.8a  1638  19.9ht  1689  ax6blem  1698  19.36i  1720  19.41h  1733  equsb1  1833  sbieh  1838  dveeq2or  1864  spsbim  1891  2ax17  1926  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  moanmo  2157  nfcvf  2397  neqne  2410  neneq  2424  necon3i  2450  nebidc  2482  r19.27v  2660  r19.28v  2661  vtoclgft  2854  rspcime  2917  eueq2dc  2979  cdeqcv  3025  ru  3030  sbcied2  3069  sbcralt  3108  sbcrext  3109  csbiebt  3167  csbied2  3175  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  ssid  3247  difss2  3335  ddifstab  3339  abvor0dc  3518  ssdifeq0  3577  rabsnt  3746  unisng  3910  dfnfc2  3911  ssbr  4132  a9evsep  4211  axnul  4214  rabex2  4236  intid  4316  opm  4326  opth1  4328  opth  4329  copsex4g  4339  0nelop  4340  moop2  4344  pocl  4400  swopo  4403  limeq  4474  suceq  4499  eusvnfb  4551  onintexmid  4671  nn0eln0  4718  elvvuni  4790  coss1  4885  coss2  4886  dmxpm  4952  elrnmpt1  4983  soirri  5131  relcnvtr  5256  relssdmrn  5257  cnvpom  5279  fveqeq2  5648  fsn2g  5822  funopsn  5830  fvsng  5850  isose  5962  canth  5969  riota2f  5994  riotaeqimp  5996  acexmidlemab  6012  fvoveq1  6041  0neqopab  6066  ssoprab2  6077  caovcld  6176  caovcomd  6179  caovassd  6182  caovcand  6185  caovordid  6189  caovordd  6191  caovdid  6198  caovdird  6201  caovimo  6216  f1opw  6230  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  xpexgALT  6295  op1stg  6313  op2ndg  6314  releldm2  6348  opabn1stprc  6358  elopabi  6360  dfmpo  6388  smoeq  6456  tfr1onlemaccex  6514  tfrcllemaccex  6527  rdgisucinc  6551  rdg0g  6554  oacl  6628  nna0r  6646  nnmsucr  6656  ercnv  6723  swoord1  6731  swoord2  6732  eqer  6734  ider  6735  iinerm  6776  brecop  6794  ixpssmapg  6897  elixpsn  6904  en1bg  6974  fundmeng  6982  rex2dom  6996  xpsneng  7006  mapen  7032  phplem3g  7042  php5  7044  php5dom  7049  findcard2d  7080  findcard2sd  7081  undifdc  7116  xpfi  7124  elfir  7172  fi0  7174  ordiso2  7234  ctssdclemr  7311  nnnninfeq2  7328  nninfisol  7332  ctssexmid  7349  nninfinfwlpo  7379  exmidaclem  7423  djuenun  7427  exmidapne  7479  cc1  7484  cc2lem  7485  mulidnq  7609  ltsonq  7618  halfnqq  7630  nqnq0pi  7658  nq02m  7685  cauappcvgprlemm  7865  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  cauappcvgpr  7882  ltposr  7983  0idsr  7987  1idsr  7988  mappsrprg  8024  ax1rid  8097  ax0id  8098  axpre-ltirr  8102  mulrid  8176  1p1times  8313  cnegexlem3  8356  pncan1  8556  npcan1  8557  kcnktkm1cn  8562  apirr  8785  recexap  8833  eqneg  8912  subrecap  9019  lediv2a  9075  nn1m1nn  9161  2txmxeqx  9275  subhalfhalf  9379  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  nn0addcl  9437  nn0mulcl  9438  zadd2cl  9609  nn0ledivnn  10002  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xnegneg  10068  xnegid  10094  xaddid1  10097  fzss1  10298  fzssp1  10302  fzshftral  10343  0elfz  10353  nn0fz0  10354  elfz0add  10355  fz0tp  10357  elfzoelz  10382  fzoval  10383  fzoss2  10409  fzossrbm1  10410  fzouzsplit  10416  elfzo1  10431  fzonn0p1  10457  fzossfzop1  10458  fzoend  10468  fzosplitsn  10479  fvinim0ffz  10488  2tnp1ge0ge0  10562  fldiv4p1lem1div2  10566  frec2uzltd  10666  frec2uzrand  10668  uzenom  10688  frecfzennn  10689  seqeq1  10713  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqk  10770  seq3f1olemstep  10777  seq3f1olemp  10778  seq3f1oleml  10779  seqf1oglem2  10783  seq3id  10788  seq3id2  10789  ser0f  10797  m1expcl2  10824  sqoddm1div8  10956  mulsubdivbinom2ap  10974  faclbnd  11004  facubnd  11008  bcpasc  11029  hashcl  11044  omgadd  11066  snopiswrd  11127  elovmpowrd  11159  lswwrd  11164  ccatval1  11178  ccatsymb  11183  ccatass  11189  ccat1st1st  11222  swrdf  11240  pfxsuff1eqwrdeq  11284  ccatpfx  11286  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccatin2d  11329  reuccatpfxs1lem  11331  s3eq2  11362  reval  11414  imval  11415  crim  11423  replim  11424  rexuz3  11555  absval  11566  sqrt0  11569  resqrexlemp1rp  11571  resqrexlemfp1  11574  resqrex  11591  abs00  11629  leabs  11639  absimle  11649  cau3  11680  dfabsmax  11782  climshft  11869  fsum3  11953  fsumcnv  12003  fsumiun  12043  binom  12050  bcxmaslem1  12054  isumshft  12056  arisum  12064  arisum2  12065  trireciplem  12066  trirecip  12067  geo2sum2  12081  geo2lim  12082  prodf1f  12109  prod0  12151  fprodfac  12181  ege2le3  12237  ef4p  12260  efgt1p2  12261  efgt1p  12262  sinval  12268  cosval  12269  negdvdsb  12373  dvdsnegb  12374  dvdsssfz1  12418  dvds1  12419  3dvds  12430  even2n  12440  oddge22np1  12447  2tp1odd  12450  ltoddhalfle  12459  m1expo  12466  m1exp1  12467  flodddiv4  12502  bits0e  12515  bits0o  12516  bitsp1e  12518  bitsp1o  12519  bitsfzo  12521  bitsinv1lem  12527  bitsinv1  12528  gcdsupex  12533  gcdsupcl  12534  alginv  12624  algcvg  12625  algcvga  12628  algfx  12629  eucalgcvga  12635  lcmdvds  12656  pw2dvds  12743  oddpwdclemodd  12749  phimul  12803  eulerth  12810  pc2dvds  12908  pcz  12910  pcmpt  12921  pcmptdvds  12923  fldivp1  12926  oddprmdvds  12932  pockthg  12935  pockthi  12936  1arith  12945  zgz  12951  4sqlem19  12987  evenennn  13019  ennnfonelemp1  13032  ennnfonelemkh  13038  ennnfonelemnn0  13048  ssnnctlemct  13072  strslfv2  13131  strslfv  13132  basm  13149  ressvalsets  13152  ressbasid  13158  pwsval  13379  qusex  13413  xpsfeq  13433  intopsn  13455  mgmidmo  13460  ismgmid  13465  mgmlrid  13467  lidrideqd  13469  lidrididd  13470  grpinvalem  13473  grpinva  13474  gsum0g  13484  issgrp  13491  imasmnd2  13540  mnd1  13543  mnd1id  13544  idmhm  13557  issubm  13560  0mhm  13574  resmhm  13575  resmhm2  13576  resmhm2b  13577  dfgrp2  13615  isgrpid2  13628  grpidd2  13629  grpinvval  13631  grpressid  13649  grpsubid1  13673  dfgrp3mlem  13686  grplactfval  13689  imasgrp2  13702  mhmlem  13706  mulgfvalg  13713  mulgnnp1  13722  mulgsubcl  13728  mulgnncl  13729  mulgnn0cl  13730  mulgcl  13731  mulgnn0z  13741  mulgneg2  13748  mulgmodid  13753  submmulg  13758  issubg  13765  subgid  13767  subgex  13768  subg0  13772  subginv  13773  subgcl  13776  subgsub  13778  subgmulg  13780  issubg3  13784  isnsg  13794  isnsg3  13799  nmzsubg  13802  nmznsg  13805  eqgval  13815  idghm  13851  resghm  13852  ghmnsgima  13860  ablressid  13927  mgpvalg  13942  rngressid  13973  ringressid  14082  imasring  14083  opprvalg  14088  opprsubgg  14103  dvdsrex  14118  dvdsrtr  14121  unitinvcl  14143  unitinvinv  14144  unitlinv  14146  unitrinv  14147  issubrng  14219  subrngid  14221  issubrng2  14230  issubrg  14241  subrgid  14243  issubrg2  14261  rrgval  14282  isdomn  14289  lmodlema  14312  islmodd  14313  rmodislmod  14371  lsssn0  14390  sraval  14457  sraring  14469  sralmod  14470  rlmvalg  14474  rlmbasg  14475  rlmplusgg  14476  rlm0g  14477  rlmsubg  14478  rlmmulrg  14479  rlmscabas  14480  rlmvscag  14481  rlmtopng  14482  rlmdsg  14483  rlmvnegg  14485  lidlss  14496  lidlssbas  14497  lidlbas  14498  crngridl  14550  zringinvg  14624  mulgrhm  14629  znval  14656  znf1o  14671  psrelbasfun  14697  mplvalcoe  14710  tsettps  14768  baspartn  14780  eltg  14782  en1top  14807  isopn3  14855  resttopon  14901  lmbr2  14944  cnptopresti  14968  cndis  14971  lmfpm  14973  lmcl  14975  lmff  14979  txswaphmeolem  15050  ispsmet  15053  psmet0  15057  xmetunirn  15088  bl2in  15133  metrest  15236  expcn  15299  cncfmptid  15327  negcncf  15335  negfcncf  15336  hovera  15377  hoverb  15378  limccl  15389  eldvap  15412  dvexp  15441  dvmptid  15446  dveflem  15456  dvef  15457  elply  15464  plypow  15474  dvply1  15495  logge0b  15620  logle1b  15622  logcxp  15627  fsumdvdsmul  15721  perfectlem2  15730  zabsle1  15734  lgsval  15739  lgsfvalg  15740  lgsval2lem  15745  lgsdir2lem2  15764  lgsdir2lem4  15766  lgsdirnn0  15782  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  gausslemma2dlem1  15796  2lgslem1a1  15821  2lgslem1a2  15822  2lgslem1b  15824  2lgslem1c  15825  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgsoddprmlem2  15841  2lgsoddprmlem3d  15845  edgfndxid  15866  uhgr0e  15939  umgrislfupgrdom  15988  ausgrusgrien  16028  egrsubgr  16120  uhgrsubgrself  16123  uhgrspanop  16139  clwwlkext2edg  16279  clwwlknccat  16280  clwwlknonmpo  16285  iseupth  16304  bj-ex  16384  bdth  16452  bj-indind  16553  gfsum0  16709