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  4230  intid  4310  opm  4320  opth1  4322  opth  4323  copsex4g  4333  0nelop  4334  moop2  4338  pocl  4394  swopo  4397  limeq  4468  suceq  4493  eusvnfb  4545  onintexmid  4665  nn0eln0  4712  elvvuni  4783  coss1  4877  coss2  4878  dmxpm  4944  elrnmpt1  4975  soirri  5123  relcnvtr  5248  relssdmrn  5249  cnvpom  5271  fveqeq2  5638  funopsn  5819  fvsng  5839  isose  5951  canth  5958  riota2f  5983  riotaeqimp  5985  acexmidlemab  6001  fvoveq1  6030  0neqopab  6055  ssoprab2  6066  caovcld  6165  caovcomd  6168  caovassd  6171  caovcand  6174  caovordid  6178  caovordd  6180  caovdid  6187  caovdird  6190  caovimo  6205  f1opw  6219  caofref  6249  caofinvl  6250  caofid0l  6251  caofid0r  6252  xpexgALT  6284  op1stg  6302  op2ndg  6303  releldm2  6337  elopabi  6347  dfmpo  6375  smoeq  6442  tfr1onlemaccex  6500  tfrcllemaccex  6513  rdgisucinc  6537  rdg0g  6540  oacl  6614  nna0r  6632  nnmsucr  6642  ercnv  6709  swoord1  6717  swoord2  6718  eqer  6720  ider  6721  iinerm  6762  brecop  6780  ixpssmapg  6883  elixpsn  6890  en1bg  6960  fundmeng  6968  rex2dom  6979  xpsneng  6989  mapen  7015  phplem3g  7025  php5  7027  php5dom  7032  findcard2d  7061  findcard2sd  7062  undifdc  7097  xpfi  7105  elfir  7151  fi0  7153  ordiso2  7213  ctssdclemr  7290  nnnninfeq2  7307  nninfisol  7311  ctssexmid  7328  nninfinfwlpo  7358  exmidaclem  7401  djuenun  7405  exmidapne  7457  cc1  7462  cc2lem  7463  mulidnq  7587  ltsonq  7596  halfnqq  7608  nqnq0pi  7636  nq02m  7663  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  cauappcvgpr  7860  ltposr  7961  0idsr  7965  1idsr  7966  mappsrprg  8002  ax1rid  8075  ax0id  8076  axpre-ltirr  8080  mulrid  8154  1p1times  8291  cnegexlem3  8334  pncan1  8534  npcan1  8535  kcnktkm1cn  8540  apirr  8763  recexap  8811  eqneg  8890  subrecap  8997  lediv2a  9053  nn1m1nn  9139  2txmxeqx  9253  subhalfhalf  9357  add1p1  9372  sub1m1  9373  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  nn0addcl  9415  nn0mulcl  9416  zadd2cl  9587  nn0ledivnn  9975  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xnegneg  10041  xnegid  10067  xaddid1  10070  fzss1  10271  fzssp1  10275  fzshftral  10316  0elfz  10326  nn0fz0  10327  elfz0add  10328  fz0tp  10330  elfzoelz  10355  fzoval  10356  fzoss2  10382  fzossrbm1  10383  fzouzsplit  10389  elfzo1  10403  fzonn0p1  10429  fzossfzop1  10430  fzoend  10440  fzosplitsn  10451  fvinim0ffz  10459  2tnp1ge0ge0  10533  fldiv4p1lem1div2  10537  frec2uzltd  10637  frec2uzrand  10639  uzenom  10659  frecfzennn  10660  seqeq1  10684  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqk  10741  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem2  10754  seq3id  10759  seq3id2  10760  ser0f  10768  m1expcl2  10795  sqoddm1div8  10927  mulsubdivbinom2ap  10945  faclbnd  10975  facubnd  10979  bcpasc  11000  hashcl  11015  omgadd  11036  snopiswrd  11094  elovmpowrd  11126  lswwrd  11131  ccatval1  11145  ccatsymb  11150  ccatass  11156  ccat1st1st  11187  swrdf  11202  pfxsuff1eqwrdeq  11246  ccatpfx  11248  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccatin2d  11291  reuccatpfxs1lem  11293  s3eq2  11324  reval  11375  imval  11376  crim  11384  replim  11385  rexuz3  11516  absval  11527  sqrt0  11530  resqrexlemp1rp  11532  resqrexlemfp1  11535  resqrex  11552  abs00  11590  leabs  11600  absimle  11610  cau3  11641  dfabsmax  11743  climshft  11830  fsum3  11913  fsumcnv  11963  fsumiun  12003  binom  12010  bcxmaslem1  12014  isumshft  12016  arisum  12024  arisum2  12025  trireciplem  12026  trirecip  12027  geo2sum2  12041  geo2lim  12042  prodf1f  12069  prod0  12111  fprodfac  12141  ege2le3  12197  ef4p  12220  efgt1p2  12221  efgt1p  12222  sinval  12228  cosval  12229  negdvdsb  12333  dvdsnegb  12334  dvdsssfz1  12378  dvds1  12379  3dvds  12390  even2n  12400  oddge22np1  12407  2tp1odd  12410  ltoddhalfle  12419  m1expo  12426  m1exp1  12427  flodddiv4  12462  bits0e  12475  bits0o  12476  bitsp1e  12478  bitsp1o  12479  bitsfzo  12481  bitsinv1lem  12487  bitsinv1  12488  gcdsupex  12493  gcdsupcl  12494  alginv  12584  algcvg  12585  algcvga  12588  algfx  12589  eucalgcvga  12595  lcmdvds  12616  pw2dvds  12703  oddpwdclemodd  12709  phimul  12763  eulerth  12770  pc2dvds  12868  pcz  12870  pcmpt  12881  pcmptdvds  12883  fldivp1  12886  oddprmdvds  12892  pockthg  12895  pockthi  12896  1arith  12905  zgz  12911  4sqlem19  12947  evenennn  12979  ennnfonelemp1  12992  ennnfonelemkh  12998  ennnfonelemnn0  13008  ssnnctlemct  13032  strslfv2  13091  strslfv  13092  basm  13109  ressvalsets  13112  ressbasid  13118  pwsval  13339  qusex  13373  xpsfeq  13393  intopsn  13415  mgmidmo  13420  ismgmid  13425  mgmlrid  13427  lidrideqd  13429  lidrididd  13430  grpinvalem  13433  grpinva  13434  gsum0g  13444  issgrp  13451  imasmnd2  13500  mnd1  13503  mnd1id  13504  idmhm  13517  issubm  13520  0mhm  13534  resmhm  13535  resmhm2  13536  resmhm2b  13537  dfgrp2  13575  isgrpid2  13588  grpidd2  13589  grpinvval  13591  grpressid  13609  grpsubid1  13633  dfgrp3mlem  13646  grplactfval  13649  imasgrp2  13662  mhmlem  13666  mulgfvalg  13673  mulgnnp1  13682  mulgsubcl  13688  mulgnncl  13689  mulgnn0cl  13690  mulgcl  13691  mulgnn0z  13701  mulgneg2  13708  mulgmodid  13713  submmulg  13718  issubg  13725  subgid  13727  subgex  13728  subg0  13732  subginv  13733  subgcl  13736  subgsub  13738  subgmulg  13740  issubg3  13744  isnsg  13754  isnsg3  13759  nmzsubg  13762  nmznsg  13765  eqgval  13775  idghm  13811  resghm  13812  ghmnsgima  13820  ablressid  13887  mgpvalg  13901  rngressid  13932  ringressid  14041  imasring  14042  opprvalg  14047  opprsubgg  14062  dvdsrex  14077  dvdsrtr  14080  unitinvcl  14102  unitinvinv  14103  unitlinv  14105  unitrinv  14106  issubrng  14178  subrngid  14180  issubrng2  14189  issubrg  14200  subrgid  14202  issubrg2  14220  rrgval  14241  isdomn  14248  lmodlema  14271  islmodd  14272  rmodislmod  14330  lsssn0  14349  sraval  14416  sraring  14428  sralmod  14429  rlmvalg  14433  rlmbasg  14434  rlmplusgg  14435  rlm0g  14436  rlmsubg  14437  rlmmulrg  14438  rlmscabas  14439  rlmvscag  14440  rlmtopng  14441  rlmdsg  14442  rlmvnegg  14444  lidlss  14455  lidlssbas  14456  lidlbas  14457  crngridl  14509  zringinvg  14583  mulgrhm  14588  znval  14615  znf1o  14630  psrelbasfun  14656  mplvalcoe  14669  tsettps  14727  baspartn  14739  eltg  14741  en1top  14766  isopn3  14814  resttopon  14860  lmbr2  14903  cnptopresti  14927  cndis  14930  lmfpm  14932  lmcl  14934  lmff  14938  txswaphmeolem  15009  ispsmet  15012  psmet0  15016  xmetunirn  15047  bl2in  15092  metrest  15195  expcn  15258  cncfmptid  15286  negcncf  15294  negfcncf  15295  hovera  15336  hoverb  15337  limccl  15348  eldvap  15371  dvexp  15400  dvmptid  15405  dveflem  15415  dvef  15416  elply  15423  plypow  15433  dvply1  15454  logge0b  15579  logle1b  15581  logcxp  15586  fsumdvdsmul  15680  perfectlem2  15689  zabsle1  15693  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsdir2lem2  15723  lgsdir2lem4  15725  lgsdirnn0  15741  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  gausslemma2dlem1  15755  2lgslem1a1  15780  2lgslem1a2  15781  2lgslem1b  15783  2lgslem1c  15784  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem2  15800  2lgsoddprmlem3d  15804  edgfndxid  15825  uhgr0e  15897  umgrislfupgrdom  15944  ausgrusgrien  15984  bj-ex  16181  bdth  16249  bj-indind  16350