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  1833  sbieh  1838  dveeq2or  1864  spsbim  1891  2ax17  1926  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  moanmo  2157  nfcvf  2398  neqne  2411  neneq  2425  necon3i  2451  nebidc  2483  r19.27v  2661  r19.28v  2662  vtoclgft  2855  rspcime  2918  eueq2dc  2980  cdeqcv  3026  ru  3031  sbcied2  3070  sbcralt  3109  sbcrext  3110  csbiebt  3168  csbied2  3176  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  ssid  3248  difss2  3337  ddifstab  3341  abvor0dc  3520  ssdifeq0  3579  rabsnt  3750  unisng  3915  dfnfc2  3916  ssbr  4137  a9evsep  4216  axnul  4219  rabex2  4241  intid  4322  opm  4332  opth1  4334  opth  4335  copsex4g  4345  0nelop  4346  moop2  4350  pocl  4406  swopo  4409  limeq  4480  suceq  4505  eusvnfb  4557  onintexmid  4677  nn0eln0  4724  elvvuni  4796  coss1  4891  coss2  4892  dmxpm  4958  elrnmpt1  4989  soirri  5138  relcnvtr  5263  relssdmrn  5264  cnvpom  5286  fveqeq2  5657  fsn2g  5830  funopsn  5838  fvsng  5858  isose  5972  canth  5979  riota2f  6004  riotaeqimp  6006  acexmidlemab  6022  fvoveq1  6051  0neqopab  6076  ssoprab2  6087  caovcld  6186  caovcomd  6189  caovassd  6192  caovcand  6195  caovordid  6199  caovordd  6201  caovdid  6208  caovdird  6211  caovimo  6226  f1opw  6240  caofref  6269  caofinvl  6270  caofid0l  6271  caofid0r  6272  xpexgALT  6304  op1stg  6322  op2ndg  6323  releldm2  6357  opabn1stprc  6367  elopabi  6369  dfmpo  6397  smoeq  6499  tfr1onlemaccex  6557  tfrcllemaccex  6570  rdgisucinc  6594  rdg0g  6597  oacl  6671  nna0r  6689  nnmsucr  6699  ercnv  6766  swoord1  6774  swoord2  6775  eqer  6777  ider  6778  iinerm  6819  brecop  6837  ixpssmapg  6940  elixpsn  6947  en1bg  7017  fundmeng  7025  rex2dom  7039  xpsneng  7049  mapen  7075  phplem3g  7085  php5  7087  php5dom  7092  findcard2d  7123  findcard2sd  7124  undifdc  7159  xpfi  7167  elfir  7215  fi0  7217  ordiso2  7277  ctssdclemr  7354  nnnninfeq2  7371  nninfisol  7375  ctssexmid  7392  nninfinfwlpo  7422  exmidaclem  7466  djuenun  7470  exmidapne  7522  cc1  7527  cc2lem  7528  mulidnq  7652  ltsonq  7661  halfnqq  7673  nqnq0pi  7701  nq02m  7728  cauappcvgprlemm  7908  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem2  7923  cauappcvgpr  7925  ltposr  8026  0idsr  8030  1idsr  8031  mappsrprg  8067  ax1rid  8140  ax0id  8141  axpre-ltirr  8145  mulrid  8219  1p1times  8355  cnegexlem3  8398  pncan1  8598  npcan1  8599  kcnktkm1cn  8604  apirr  8827  recexap  8875  eqneg  8954  subrecap  9061  lediv2a  9117  nn1m1nn  9203  2txmxeqx  9317  subhalfhalf  9421  add1p1  9436  sub1m1  9437  cnm2m1cnm3  9438  xp1d2m1eqxm1d2  9439  div4p1lem1div2  9440  nn0addcl  9479  nn0mulcl  9480  zadd2cl  9653  nn0ledivnn  10046  nltpnft  10093  ngtmnft  10096  xrrebnd  10098  xnegneg  10112  xnegid  10138  xaddid1  10141  fzss1  10343  fzssp1  10347  fzshftral  10388  0elfz  10398  nn0fz0  10399  elfz0add  10400  fz0tp  10402  elfzoelz  10427  fzoval  10428  fzoss2  10454  fzossrbm1  10455  fzouzsplit  10461  elfzo1  10476  fzonn0p1  10502  fzossfzop1  10503  fzoend  10513  fzosplitsn  10524  fvinim0ffz  10533  2tnp1ge0ge0  10607  fldiv4p1lem1div2  10611  frec2uzltd  10711  frec2uzrand  10713  uzenom  10733  frecfzennn  10734  seqeq1  10758  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqk  10815  seq3f1olemstep  10822  seq3f1olemp  10823  seq3f1oleml  10824  seqf1oglem2  10828  seq3id  10833  seq3id2  10834  ser0f  10842  m1expcl2  10869  sqoddm1div8  11001  mulsubdivbinom2ap  11019  faclbnd  11049  facubnd  11053  bcpasc  11074  hashcl  11089  omgadd  11111  snopiswrd  11172  elovmpowrd  11204  lswwrd  11209  ccatval1  11223  ccatsymb  11228  ccatass  11234  ccat1st1st  11267  swrdf  11285  pfxsuff1eqwrdeq  11329  ccatpfx  11331  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccatin2d  11374  reuccatpfxs1lem  11376  s3eq2  11407  reval  11472  imval  11473  crim  11481  replim  11482  rexuz3  11613  absval  11624  sqrt0  11627  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrex  11649  abs00  11687  leabs  11697  absimle  11707  cau3  11738  dfabsmax  11840  climshft  11927  fsum3  12011  fsumcnv  12061  fsumiun  12101  binom  12108  bcxmaslem1  12112  isumshft  12114  arisum  12122  arisum2  12123  trireciplem  12124  trirecip  12125  geo2sum2  12139  geo2lim  12140  prodf1f  12167  prod0  12209  fprodfac  12239  ege2le3  12295  ef4p  12318  efgt1p2  12319  efgt1p  12320  sinval  12326  cosval  12327  negdvdsb  12431  dvdsnegb  12432  dvdsssfz1  12476  dvds1  12477  3dvds  12488  even2n  12498  oddge22np1  12505  2tp1odd  12508  ltoddhalfle  12517  m1expo  12524  m1exp1  12525  flodddiv4  12560  bits0e  12573  bits0o  12574  bitsp1e  12576  bitsp1o  12577  bitsfzo  12579  bitsinv1lem  12585  bitsinv1  12586  gcdsupex  12591  gcdsupcl  12592  alginv  12682  algcvg  12683  algcvga  12686  algfx  12687  eucalgcvga  12693  lcmdvds  12714  pw2dvds  12801  oddpwdclemodd  12807  phimul  12861  eulerth  12868  pc2dvds  12966  pcz  12968  pcmpt  12979  pcmptdvds  12981  fldivp1  12984  oddprmdvds  12990  pockthg  12993  pockthi  12994  1arith  13003  zgz  13009  4sqlem19  13045  evenennn  13077  ennnfonelemp1  13090  ennnfonelemkh  13096  ennnfonelemnn0  13106  ssnnctlemct  13130  strslfv2  13189  strslfv  13190  basm  13207  ressvalsets  13210  ressbasid  13216  pwsval  13437  qusex  13471  xpsfeq  13491  intopsn  13513  mgmidmo  13518  ismgmid  13523  mgmlrid  13525  lidrideqd  13527  lidrididd  13528  grpinvalem  13531  grpinva  13532  gsum0g  13542  issgrp  13549  imasmnd2  13598  mnd1  13601  mnd1id  13602  idmhm  13615  issubm  13618  0mhm  13632  resmhm  13633  resmhm2  13634  resmhm2b  13635  dfgrp2  13673  isgrpid2  13686  grpidd2  13687  grpinvval  13689  grpressid  13707  grpsubid1  13731  dfgrp3mlem  13744  grplactfval  13747  imasgrp2  13760  mhmlem  13764  mulgfvalg  13771  mulgnnp1  13780  mulgsubcl  13786  mulgnncl  13787  mulgnn0cl  13788  mulgcl  13789  mulgnn0z  13799  mulgneg2  13806  mulgmodid  13811  submmulg  13816  issubg  13823  subgid  13825  subgex  13826  subg0  13830  subginv  13831  subgcl  13834  subgsub  13836  subgmulg  13838  issubg3  13842  isnsg  13852  isnsg3  13857  nmzsubg  13860  nmznsg  13863  eqgval  13873  idghm  13909  resghm  13910  ghmnsgima  13918  ablressid  13985  mgpvalg  14000  rngressid  14031  ringressid  14140  imasring  14141  opprvalg  14146  opprsubgg  14161  dvdsrex  14176  dvdsrtr  14179  unitinvcl  14201  unitinvinv  14202  unitlinv  14204  unitrinv  14205  issubrng  14277  subrngid  14279  issubrng2  14288  issubrg  14299  subrgid  14301  issubrg2  14319  rrgval  14340  isdomn  14348  lmodlema  14371  islmodd  14372  rmodislmod  14430  lsssn0  14449  sraval  14516  sraring  14528  sralmod  14529  rlmvalg  14533  rlmbasg  14534  rlmplusgg  14535  rlm0g  14536  rlmsubg  14537  rlmmulrg  14538  rlmscabas  14539  rlmvscag  14540  rlmtopng  14541  rlmdsg  14542  rlmvnegg  14544  lidlss  14555  lidlssbas  14556  lidlbas  14557  crngridl  14609  zringinvg  14683  mulgrhm  14688  znval  14715  znf1o  14730  psrbaglesupp  14752  psrbaglecl  14754  psrbagcon  14755  psrelbasfun  14761  mplvalcoe  14774  tsettps  14832  baspartn  14844  eltg  14846  en1top  14871  isopn3  14919  resttopon  14965  lmbr2  15008  cnptopresti  15032  cndis  15035  lmfpm  15037  lmcl  15039  lmff  15043  txswaphmeolem  15114  ispsmet  15117  psmet0  15121  xmetunirn  15152  bl2in  15197  metrest  15300  expcn  15363  cncfmptid  15391  negcncf  15399  negfcncf  15400  hovera  15441  hoverb  15442  limccl  15453  eldvap  15476  dvexp  15505  dvmptid  15510  dveflem  15520  dvef  15521  elply  15528  plypow  15538  dvply1  15559  logge0b  15684  logle1b  15686  logcxp  15691  fsumdvdsmul  15788  perfectlem2  15797  zabsle1  15801  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsdir2lem2  15831  lgsdir2lem4  15833  lgsdirnn0  15849  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  gausslemma2dlem1  15863  2lgslem1a1  15888  2lgslem1a2  15889  2lgslem1b  15891  2lgslem1c  15892  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgsoddprmlem2  15908  2lgsoddprmlem3d  15912  edgfndxid  15933  uhgr0e  16006  umgrislfupgrdom  16055  ausgrusgrien  16095  egrsubgr  16187  uhgrsubgrself  16190  uhgrspanop  16206  clwwlkext2edg  16346  clwwlknccat  16347  clwwlknonmpo  16352  iseupth  16371  bj-ex  16463  bdth  16530  bj-indind  16631  exmidcon  16711  exmidpeirce  16712  gfsum0  16794