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  3905  dfnfc2  3906  ssbr  4127  a9evsep  4206  axnul  4209  rabex2  4231  intid  4311  opm  4321  opth1  4323  opth  4324  copsex4g  4334  0nelop  4335  moop2  4339  pocl  4395  swopo  4398  limeq  4469  suceq  4494  eusvnfb  4546  onintexmid  4666  nn0eln0  4713  elvvuni  4785  coss1  4880  coss2  4881  dmxpm  4947  elrnmpt1  4978  soirri  5126  relcnvtr  5251  relssdmrn  5252  cnvpom  5274  fveqeq2  5641  funopsn  5822  fvsng  5842  isose  5954  canth  5961  riota2f  5986  riotaeqimp  5988  acexmidlemab  6004  fvoveq1  6033  0neqopab  6058  ssoprab2  6069  caovcld  6168  caovcomd  6171  caovassd  6174  caovcand  6177  caovordid  6181  caovordd  6183  caovdid  6190  caovdird  6193  caovimo  6208  f1opw  6222  caofref  6252  caofinvl  6253  caofid0l  6254  caofid0r  6255  xpexgALT  6287  op1stg  6305  op2ndg  6306  releldm2  6340  opabn1stprc  6350  elopabi  6352  dfmpo  6380  smoeq  6447  tfr1onlemaccex  6505  tfrcllemaccex  6518  rdgisucinc  6542  rdg0g  6545  oacl  6619  nna0r  6637  nnmsucr  6647  ercnv  6714  swoord1  6722  swoord2  6723  eqer  6725  ider  6726  iinerm  6767  brecop  6785  ixpssmapg  6888  elixpsn  6895  en1bg  6965  fundmeng  6973  rex2dom  6984  xpsneng  6994  mapen  7020  phplem3g  7030  php5  7032  php5dom  7037  findcard2d  7066  findcard2sd  7067  undifdc  7102  xpfi  7110  elfir  7156  fi0  7158  ordiso2  7218  ctssdclemr  7295  nnnninfeq2  7312  nninfisol  7316  ctssexmid  7333  nninfinfwlpo  7363  exmidaclem  7406  djuenun  7410  exmidapne  7462  cc1  7467  cc2lem  7468  mulidnq  7592  ltsonq  7601  halfnqq  7613  nqnq0pi  7641  nq02m  7668  cauappcvgprlemm  7848  cauappcvgprlemloc  7855  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlem2  7863  cauappcvgpr  7865  ltposr  7966  0idsr  7970  1idsr  7971  mappsrprg  8007  ax1rid  8080  ax0id  8081  axpre-ltirr  8085  mulrid  8159  1p1times  8296  cnegexlem3  8339  pncan1  8539  npcan1  8540  kcnktkm1cn  8545  apirr  8768  recexap  8816  eqneg  8895  subrecap  9002  lediv2a  9058  nn1m1nn  9144  2txmxeqx  9258  subhalfhalf  9362  add1p1  9377  sub1m1  9378  cnm2m1cnm3  9379  xp1d2m1eqxm1d2  9380  div4p1lem1div2  9381  nn0addcl  9420  nn0mulcl  9421  zadd2cl  9592  nn0ledivnn  9980  nltpnft  10027  ngtmnft  10030  xrrebnd  10032  xnegneg  10046  xnegid  10072  xaddid1  10075  fzss1  10276  fzssp1  10280  fzshftral  10321  0elfz  10331  nn0fz0  10332  elfz0add  10333  fz0tp  10335  elfzoelz  10360  fzoval  10361  fzoss2  10387  fzossrbm1  10388  fzouzsplit  10394  elfzo1  10408  fzonn0p1  10434  fzossfzop1  10435  fzoend  10445  fzosplitsn  10456  fvinim0ffz  10464  2tnp1ge0ge0  10538  fldiv4p1lem1div2  10542  frec2uzltd  10642  frec2uzrand  10644  uzenom  10664  frecfzennn  10665  seqeq1  10689  iseqf1olemkle  10736  iseqf1olemklt  10737  iseqf1olemqk  10746  seq3f1olemstep  10753  seq3f1olemp  10754  seq3f1oleml  10755  seqf1oglem2  10759  seq3id  10764  seq3id2  10765  ser0f  10773  m1expcl2  10800  sqoddm1div8  10932  mulsubdivbinom2ap  10950  faclbnd  10980  facubnd  10984  bcpasc  11005  hashcl  11020  omgadd  11041  snopiswrd  11099  elovmpowrd  11131  lswwrd  11136  ccatval1  11150  ccatsymb  11155  ccatass  11161  ccat1st1st  11193  swrdf  11208  pfxsuff1eqwrdeq  11252  ccatpfx  11254  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12  11286  swrdccatin2d  11297  reuccatpfxs1lem  11299  s3eq2  11330  reval  11381  imval  11382  crim  11390  replim  11391  rexuz3  11522  absval  11533  sqrt0  11536  resqrexlemp1rp  11538  resqrexlemfp1  11541  resqrex  11558  abs00  11596  leabs  11606  absimle  11616  cau3  11647  dfabsmax  11749  climshft  11836  fsum3  11919  fsumcnv  11969  fsumiun  12009  binom  12016  bcxmaslem1  12020  isumshft  12022  arisum  12030  arisum2  12031  trireciplem  12032  trirecip  12033  geo2sum2  12047  geo2lim  12048  prodf1f  12075  prod0  12117  fprodfac  12147  ege2le3  12203  ef4p  12226  efgt1p2  12227  efgt1p  12228  sinval  12234  cosval  12235  negdvdsb  12339  dvdsnegb  12340  dvdsssfz1  12384  dvds1  12385  3dvds  12396  even2n  12406  oddge22np1  12413  2tp1odd  12416  ltoddhalfle  12425  m1expo  12432  m1exp1  12433  flodddiv4  12468  bits0e  12481  bits0o  12482  bitsp1e  12484  bitsp1o  12485  bitsfzo  12487  bitsinv1lem  12493  bitsinv1  12494  gcdsupex  12499  gcdsupcl  12500  alginv  12590  algcvg  12591  algcvga  12594  algfx  12595  eucalgcvga  12601  lcmdvds  12622  pw2dvds  12709  oddpwdclemodd  12715  phimul  12769  eulerth  12776  pc2dvds  12874  pcz  12876  pcmpt  12887  pcmptdvds  12889  fldivp1  12892  oddprmdvds  12898  pockthg  12901  pockthi  12902  1arith  12911  zgz  12917  4sqlem19  12953  evenennn  12985  ennnfonelemp1  12998  ennnfonelemkh  13004  ennnfonelemnn0  13014  ssnnctlemct  13038  strslfv2  13097  strslfv  13098  basm  13115  ressvalsets  13118  ressbasid  13124  pwsval  13345  qusex  13379  xpsfeq  13399  intopsn  13421  mgmidmo  13426  ismgmid  13431  mgmlrid  13433  lidrideqd  13435  lidrididd  13436  grpinvalem  13439  grpinva  13440  gsum0g  13450  issgrp  13457  imasmnd2  13506  mnd1  13509  mnd1id  13510  idmhm  13523  issubm  13526  0mhm  13540  resmhm  13541  resmhm2  13542  resmhm2b  13543  dfgrp2  13581  isgrpid2  13594  grpidd2  13595  grpinvval  13597  grpressid  13615  grpsubid1  13639  dfgrp3mlem  13652  grplactfval  13655  imasgrp2  13668  mhmlem  13672  mulgfvalg  13679  mulgnnp1  13688  mulgsubcl  13694  mulgnncl  13695  mulgnn0cl  13696  mulgcl  13697  mulgnn0z  13707  mulgneg2  13714  mulgmodid  13719  submmulg  13724  issubg  13731  subgid  13733  subgex  13734  subg0  13738  subginv  13739  subgcl  13742  subgsub  13744  subgmulg  13746  issubg3  13750  isnsg  13760  isnsg3  13765  nmzsubg  13768  nmznsg  13771  eqgval  13781  idghm  13817  resghm  13818  ghmnsgima  13826  ablressid  13893  mgpvalg  13907  rngressid  13938  ringressid  14047  imasring  14048  opprvalg  14053  opprsubgg  14068  dvdsrex  14083  dvdsrtr  14086  unitinvcl  14108  unitinvinv  14109  unitlinv  14111  unitrinv  14112  issubrng  14184  subrngid  14186  issubrng2  14195  issubrg  14206  subrgid  14208  issubrg2  14226  rrgval  14247  isdomn  14254  lmodlema  14277  islmodd  14278  rmodislmod  14336  lsssn0  14355  sraval  14422  sraring  14434  sralmod  14435  rlmvalg  14439  rlmbasg  14440  rlmplusgg  14441  rlm0g  14442  rlmsubg  14443  rlmmulrg  14444  rlmscabas  14445  rlmvscag  14446  rlmtopng  14447  rlmdsg  14448  rlmvnegg  14450  lidlss  14461  lidlssbas  14462  lidlbas  14463  crngridl  14515  zringinvg  14589  mulgrhm  14594  znval  14621  znf1o  14636  psrelbasfun  14662  mplvalcoe  14675  tsettps  14733  baspartn  14745  eltg  14747  en1top  14772  isopn3  14820  resttopon  14866  lmbr2  14909  cnptopresti  14933  cndis  14936  lmfpm  14938  lmcl  14940  lmff  14944  txswaphmeolem  15015  ispsmet  15018  psmet0  15022  xmetunirn  15053  bl2in  15098  metrest  15201  expcn  15264  cncfmptid  15292  negcncf  15300  negfcncf  15301  hovera  15342  hoverb  15343  limccl  15354  eldvap  15377  dvexp  15406  dvmptid  15411  dveflem  15421  dvef  15422  elply  15429  plypow  15439  dvply1  15460  logge0b  15585  logle1b  15587  logcxp  15592  fsumdvdsmul  15686  perfectlem2  15695  zabsle1  15699  lgsval  15704  lgsfvalg  15705  lgsval2lem  15710  lgsdir2lem2  15729  lgsdir2lem4  15731  lgsdirnn0  15747  gausslemma2dlem0i  15757  gausslemma2dlem1a  15758  gausslemma2dlem1  15761  2lgslem1a1  15786  2lgslem1a2  15787  2lgslem1b  15789  2lgslem1c  15790  2lgslem3a  15793  2lgslem3b  15794  2lgslem3c  15795  2lgslem3d  15796  2lgsoddprmlem2  15806  2lgsoddprmlem3d  15810  edgfndxid  15831  uhgr0e  15903  umgrislfupgrdom  15950  ausgrusgrien  15990  clwwlkext2edg  16190  clwwlknccat  16191  bj-ex  16235  bdth  16303  bj-indind  16404