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  597  pm5.36  610  con2i  628  notnot  630  con3i  633  biijust  642  con3  643  con2  644  pm5.19  707  olc  712  orc  713  pm2.621  748  pm1.2  757  orim1i  761  orim2i  762  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  orim2  790  orbi1  793  pm2.38  804  pm2.74  808  pm3.2ni  814  biort  830  dcbiit  840  pm4.79dc  904  dcand  934  biantr  954  3anim1i  1187  3anim2i  1188  3anim3i  1189  mpd3an23  1350  trujust  1366  tru  1368  dftru2  1372  truimtru  1420  falimfal  1423  3impexp  1448  19.26  1495  19.8a  1604  19.9ht  1655  ax6blem  1664  19.36i  1686  19.41h  1699  equsb1  1799  sbieh  1804  dveeq2or  1830  spsbim  1857  2ax17  1892  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  moanmo  2122  nfcvf  2362  neqne  2375  neneq  2389  necon3i  2415  nebidc  2447  r19.27v  2624  r19.28v  2625  vtoclgft  2814  rspcime  2875  eueq2dc  2937  cdeqcv  2983  ru  2988  sbcied2  3027  sbcralt  3066  sbcrext  3067  csbiebt  3124  csbied2  3132  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  ssid  3204  difss2  3292  ddifstab  3296  abvor0dc  3475  ssdifeq0  3534  rabsnt  3698  unisng  3857  dfnfc2  3858  a9evsep  4156  axnul  4159  rabex2  4180  intid  4258  opm  4268  opth1  4270  opth  4271  copsex4g  4281  0nelop  4282  moop2  4285  pocl  4339  swopo  4342  limeq  4413  suceq  4438  eusvnfb  4490  onintexmid  4610  nn0eln0  4657  elvvuni  4728  coss1  4822  coss2  4823  dmxpm  4887  elrnmpt1  4918  soirri  5065  relcnvtr  5190  relssdmrn  5191  cnvpom  5213  fveqeq2  5570  fvsng  5761  isose  5871  canth  5878  riota2f  5902  acexmidlemab  5919  fvoveq1  5948  0neqopab  5971  ssoprab2  5982  caovcld  6081  caovcomd  6084  caovassd  6087  caovcand  6090  caovordid  6094  caovordd  6096  caovdid  6103  caovdird  6106  caovimo  6121  f1opw  6134  caofref  6164  caofinvl  6165  caofid0l  6166  caofid0r  6167  xpexgALT  6199  op1stg  6217  op2ndg  6218  releldm2  6252  elopabi  6262  dfmpo  6290  smoeq  6357  tfr1onlemaccex  6415  tfrcllemaccex  6428  rdgisucinc  6452  rdg0g  6455  oacl  6527  nna0r  6545  nnmsucr  6555  ercnv  6622  swoord1  6630  swoord2  6631  eqer  6633  ider  6634  iinerm  6675  brecop  6693  ixpssmapg  6796  elixpsn  6803  en1bg  6868  fundmeng  6875  xpsneng  6890  mapen  6916  phplem3g  6926  php5  6928  php5dom  6933  findcard2d  6961  findcard2sd  6962  undifdc  6994  xpfi  7002  elfir  7048  fi0  7050  ordiso2  7110  ctssdclemr  7187  nnnninfeq2  7204  nninfisol  7208  ctssexmid  7225  nninfinfwlpo  7255  exmidaclem  7293  djuenun  7297  exmidapne  7345  cc1  7350  cc2lem  7351  mulidnq  7475  ltsonq  7484  halfnqq  7496  nqnq0pi  7524  nq02m  7551  cauappcvgprlemm  7731  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem2  7746  cauappcvgpr  7748  ltposr  7849  0idsr  7853  1idsr  7854  mappsrprg  7890  ax1rid  7963  ax0id  7964  axpre-ltirr  7968  mulrid  8042  1p1times  8179  cnegexlem3  8222  pncan1  8422  npcan1  8423  kcnktkm1cn  8428  apirr  8651  recexap  8699  eqneg  8778  subrecap  8885  lediv2a  8941  nn1m1nn  9027  2txmxeqx  9141  subhalfhalf  9245  add1p1  9260  sub1m1  9261  cnm2m1cnm3  9262  xp1d2m1eqxm1d2  9263  div4p1lem1div2  9264  nn0addcl  9303  nn0mulcl  9304  zadd2cl  9474  nn0ledivnn  9861  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xnegneg  9927  xnegid  9953  xaddid1  9956  fzss1  10157  fzssp1  10161  fzshftral  10202  0elfz  10212  nn0fz0  10213  elfz0add  10214  fz0tp  10216  elfzoelz  10241  fzoval  10242  fzoss2  10267  fzossrbm1  10268  fzouzsplit  10274  elfzo1  10285  fzonn0p1  10306  fzossfzop1  10307  fzoend  10317  fzosplitsn  10328  fvinim0ffz  10336  2tnp1ge0ge0  10410  fldiv4p1lem1div2  10414  frec2uzltd  10514  frec2uzrand  10516  uzenom  10536  frecfzennn  10537  seqeq1  10561  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqk  10618  seq3f1olemstep  10625  seq3f1olemp  10626  seq3f1oleml  10627  seqf1oglem2  10631  seq3id  10636  seq3id2  10637  ser0f  10645  m1expcl2  10672  sqoddm1div8  10804  mulsubdivbinom2ap  10822  faclbnd  10852  facubnd  10856  bcpasc  10877  hashcl  10892  omgadd  10913  snopiswrd  10964  elovmpowrd  10995  reval  11033  imval  11034  crim  11042  replim  11043  rexuz3  11174  absval  11185  sqrt0  11188  resqrexlemp1rp  11190  resqrexlemfp1  11193  resqrex  11210  abs00  11248  leabs  11258  absimle  11268  cau3  11299  dfabsmax  11401  climshft  11488  fsum3  11571  fsumcnv  11621  fsumiun  11661  binom  11668  bcxmaslem1  11672  isumshft  11674  arisum  11682  arisum2  11683  trireciplem  11684  trirecip  11685  geo2sum2  11699  geo2lim  11700  prodf1f  11727  prod0  11769  fprodfac  11799  ege2le3  11855  ef4p  11878  efgt1p2  11879  efgt1p  11880  sinval  11886  cosval  11887  negdvdsb  11991  dvdsnegb  11992  dvdsssfz1  12036  dvds1  12037  3dvds  12048  even2n  12058  oddge22np1  12065  2tp1odd  12068  ltoddhalfle  12077  m1expo  12084  m1exp1  12085  flodddiv4  12120  bits0e  12133  bits0o  12134  bitsp1e  12136  bitsp1o  12137  bitsfzo  12139  bitsinv1lem  12145  bitsinv1  12146  gcdsupex  12151  gcdsupcl  12152  alginv  12242  algcvg  12243  algcvga  12246  algfx  12247  eucalgcvga  12253  lcmdvds  12274  pw2dvds  12361  oddpwdclemodd  12367  phimul  12421  eulerth  12428  pc2dvds  12526  pcz  12528  pcmpt  12539  pcmptdvds  12541  fldivp1  12544  oddprmdvds  12550  pockthg  12553  pockthi  12554  1arith  12563  zgz  12569  4sqlem19  12605  evenennn  12637  ennnfonelemp1  12650  ennnfonelemkh  12656  ennnfonelemnn0  12666  ssnnctlemct  12690  strslfv2  12749  strslfv  12750  basm  12766  ressvalsets  12769  ressbasid  12775  pwsval  12995  qusex  13029  xpsfeq  13049  intopsn  13071  mgmidmo  13076  ismgmid  13081  mgmlrid  13083  lidrideqd  13085  lidrididd  13086  grpinvalem  13089  grpinva  13090  gsum0g  13100  issgrp  13107  imasmnd2  13156  mnd1  13159  mnd1id  13160  idmhm  13173  issubm  13176  0mhm  13190  resmhm  13191  resmhm2  13192  resmhm2b  13193  dfgrp2  13231  isgrpid2  13244  grpidd2  13245  grpinvval  13247  grpressid  13265  grpsubid1  13289  dfgrp3mlem  13302  grplactfval  13305  imasgrp2  13318  mhmlem  13322  mulgfvalg  13329  mulgnnp1  13338  mulgsubcl  13344  mulgnncl  13345  mulgnn0cl  13346  mulgcl  13347  mulgnn0z  13357  mulgneg2  13364  mulgmodid  13369  submmulg  13374  issubg  13381  subgid  13383  subgex  13384  subg0  13388  subginv  13389  subgcl  13392  subgsub  13394  subgmulg  13396  issubg3  13400  isnsg  13410  isnsg3  13415  nmzsubg  13418  nmznsg  13421  eqgval  13431  idghm  13467  resghm  13468  ghmnsgima  13476  ablressid  13543  mgpvalg  13557  rngressid  13588  ringressid  13697  imasring  13698  opprvalg  13703  opprsubgg  13718  dvdsrex  13732  dvdsrtr  13735  unitinvcl  13757  unitinvinv  13758  unitlinv  13760  unitrinv  13761  issubrng  13833  subrngid  13835  issubrng2  13844  issubrg  13855  subrgid  13857  issubrg2  13875  rrgval  13896  isdomn  13903  lmodlema  13926  islmodd  13927  rmodislmod  13985  lsssn0  14004  sraval  14071  sraring  14083  sralmod  14084  rlmvalg  14088  rlmbasg  14089  rlmplusgg  14090  rlm0g  14091  rlmsubg  14092  rlmmulrg  14093  rlmscabas  14094  rlmvscag  14095  rlmtopng  14096  rlmdsg  14097  rlmvnegg  14099  lidlss  14110  lidlssbas  14111  lidlbas  14112  crngridl  14164  zringinvg  14238  mulgrhm  14243  znval  14270  znf1o  14285  psrelbasfun  14311  mplvalcoe  14324  tsettps  14382  baspartn  14394  eltg  14396  en1top  14421  isopn3  14469  resttopon  14515  lmbr2  14558  cnptopresti  14582  cndis  14585  lmfpm  14587  lmcl  14589  lmff  14593  txswaphmeolem  14664  ispsmet  14667  psmet0  14671  xmetunirn  14702  bl2in  14747  metrest  14850  expcn  14913  cncfmptid  14941  negcncf  14949  negfcncf  14950  hovera  14991  hoverb  14992  limccl  15003  eldvap  15026  dvexp  15055  dvmptid  15060  dveflem  15070  dvef  15071  elply  15078  plypow  15088  dvply1  15109  logge0b  15234  logle1b  15236  logcxp  15241  fsumdvdsmul  15335  perfectlem2  15344  zabsle1  15348  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsdir2lem2  15378  lgsdir2lem4  15380  lgsdirnn0  15396  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2dlem1  15410  2lgslem1a1  15435  2lgslem1a2  15436  2lgslem1b  15438  2lgslem1c  15439  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgsoddprmlem2  15455  2lgsoddprmlem3d  15459  bj-ex  15516  bdth  15585  bj-indind  15686