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 ⊢ (𝜑 → 𝜑)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  399  anass  405  mpdan  425  mpancom  426  pm5.32  457  anbi1  470  anbi2  471  mpan10  478  adantl3r  516  simpll  531  simplr  533  simprl  535  simprr  537  pm3.45  605  pm5.36  618  con2i  636  notnot  638  con3i  641  biijust  650  con3  651  con2  652  pm5.19  718  olc  723  orc  724  pm2.621  759  pm1.2  768  orim1i  772  orim2i  773  pm2.41  788  pm2.42  789  pm2.4  790  pm4.44  791  orim2  801  orbi1  804  pm2.38  815  pm2.74  819  pm3.2ni  825  biort  841  dcbiit  851  pm4.79dc  915  dcand  945  biantr  965  3anim1i  1216  3anim2i  1217  3anim3i  1218  mpd3an23  1380  trujust  1404  tru  1406  dftru2  1410  truimtru  1458  falimfal  1461  3impexp  1487  19.26  1534  19.8a  1643  19.9ht  1694  hbn  1703  19.36i  1724  19.41h  1737  equsb1  1838  sbieh  1843  dveeq2or  1869  spsbim  1896  2ax17  1931  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  moanmo  2164  nfcvf  2415  neqne  2428  neneq  2442  necon3i  2468  nebidc  2500  r19.27v  2678  r19.28v  2679  vtoclgft  2873  rspcime  2937  eueq2dc  2999  cdeqcv  3045  ru  3050  sbcied2  3089  sbcralt  3128  sbcrext  3129  csbiebt  3187  csbied2  3195  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ssid  3268  difss2  3357  ddifstab  3361  abvor0dc  3545  ssdifeq0  3610  rabsnt  3786  unisng  3952  dfnfc2  3953  ssbr  4174  a9evsep  4255  axnul  4258  sepab  4278  rabex2  4282  intid  4364  opm  4374  opth1  4376  opth  4377  copsex4g  4387  0nelop  4388  moop2  4392  pocl  4448  swopo  4451  limeq  4522  suceq  4547  eusvnfb  4600  onintexmid  4720  nn0eln0  4767  elvvuni  4839  coss1  4935  coss2  4936  dmxpm  5002  elrnmpt1  5033  soirri  5182  relcnvtr  5307  relssdmrn  5308  cnvpom  5330  fveqeq2  5704  fsn2g  5883  funopsn  5891  fvsng  5911  isose  6027  canth  6036  riota2f  6061  riotaeqimp  6063  acexmidlemab  6079  fvoveq1  6108  0neqopab  6133  ssoprab2  6144  caovcld  6243  caovcomd  6246  caovassd  6249  caovcand  6252  caovordid  6256  caovordd  6258  caovdid  6265  caovdird  6268  caovimo  6283  f1opw  6297  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  xpexgALT  6366  op1stg  6384  op2ndg  6385  releldm2  6419  opabn1stprc  6429  elopabi  6431  dfmpo  6459  smoeq  6561  tfr1onlemaccex  6619  tfrcllemaccex  6632  rdgisucinc  6656  rdg0g  6659  oacl  6733  nna0r  6751  nnmsucr  6761  ercnv  6828  swoord1  6836  swoord2  6837  eqer  6839  ider  6840  iinerm  6881  brecop  6899  fsetdmprc0  6950  ixpssmapg  7010  elixpsn  7017  en1bg  7087  fundmeng  7095  rex2dom  7110  xpsneng  7120  mapen  7146  phplem3g  7157  php5  7159  php5dom  7164  findcard2d  7195  findcard2sd  7196  undifdc  7231  xpfi  7239  fsuppxpfi  7296  elfir  7307  fi0  7309  ordiso2  7375  ctssdclemr  7452  nnnninfeq2  7469  nninfisol  7473  ctssexmid  7490  nninfinfwlpo  7520  exmidaclem  7564  djuenun  7568  papeq2  7610  papirr  7611  exmidapne  7626  cc1  7631  cc2lem  7632  mulidnq  7756  ltsonq  7765  halfnqq  7777  nqnq0pi  7805  nq02m  7832  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  cauappcvgpr  8029  ltposr  8130  0idsr  8134  1idsr  8135  mappsrprg  8171  ax1rid  8244  ax0id  8245  axpre-ltirr  8249  mulrid  8323  1p1times  8461  cnegexlem3  8504  pncan1  8705  npcan1  8706  kcnktkm1cn  8711  apirr  8935  recexap  8983  msq0  8999  eqneg  9064  subrecap  9171  lediv2a  9227  nn1m1nn  9324  2txmxeqx  9438  subhalfhalf  9544  add1p1  9559  sub1m1  9560  cnm2m1cnm3  9561  xp1d2m1eqxm1d2  9562  div4p1lem1div2  9563  nn0addcl  9602  nn0mulcl  9603  zadd2cl  9779  nn0ledivnn  10178  nltpnft  10226  ngtmnft  10229  xrrebnd  10231  xnegneg  10245  xnegid  10271  xaddid1  10274  fzss1  10479  fzssp1  10483  fzshftral  10525  0elfz  10535  nn0fz0  10536  elfz0add  10537  fz0tp  10539  elfzoelz  10564  fzoval  10565  fzoss2  10591  fzossrbm1  10592  fzouzsplit  10598  elfzo1  10613  fzonn0p1  10639  fzossfzop1  10640  fzoend  10650  fzosplitsn  10661  fvinim0ffz  10670  2tnp1ge0ge0  10749  fldiv4p1lem1div2  10753  frec2uzltd  10853  frec2uzrand  10855  uzenom  10875  frecfzennn  10876  seqeq1  10900  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemqk  10957  seq3f1olemstep  10964  seq3f1olemp  10965  seq3f1oleml  10966  seqf1oglem2  10970  seq3id  10975  seq3id2  10976  ser0f  10984  m1expcl2  11011  resq01  11108  sqoddm1div8  11144  mulsubdivbinom2ap  11163  faclbnd  11193  facubnd  11197  bcpasc  11218  hashcl  11234  omgadd  11256  hashfibc  11297  snopiswrd  11328  elovmpowrd  11360  lswwrd  11365  ccatval1  11379  ccatsymb  11384  ccatass  11390  ccat1st1st  11423  swrdf  11441  pfxsuff1eqwrdeq  11485  ccatpfx  11487  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  swrdccatin2d  11530  reuccatpfxs1lem  11532  s3eq2  11563  reval  11628  imval  11629  crim  11637  replim  11638  sq01  11674  rexuz3  11770  absval  11781  sqrt0  11784  resqrexlemp1rp  11786  resqrexlemfp1  11789  resqrex  11806  abs00  11844  leabs  11854  absimle  11865  cau3  11896  dfabsmax  11998  climshft  12086  fsum3  12170  fsumcnv  12220  fsumiun  12260  binom  12267  bcxmaslem1  12271  isumshft  12273  arisum  12281  arisum2  12282  trireciplem  12283  trirecip  12284  geo2sum2  12298  geo2lim  12299  prodf1f  12326  prod0  12368  fprodfac  12398  ege2le3  12454  ef4p  12477  efgt1p2  12478  efgt1p  12479  sinval  12485  cosval  12486  negdvdsb  12590  dvdsnegb  12591  dvdsssfz1  12635  dvds1  12636  3dvds  12647  even2n  12657  oddge22np1  12664  2tp1odd  12667  ltoddhalfle  12676  m1expo  12683  m1exp1  12684  flodddiv4  12719  bits0e  12732  bits0o  12733  bitsp1e  12735  bitsp1o  12736  bitsfzo  12738  bitsinv1lem  12744  bitsinv1  12745  gcdsupex  12750  gcdsupcl  12751  alginv  12841  algcvg  12842  algcvga  12845  algfx  12846  eucalgcvga  12852  lcmdvds  12873  phimul  13024  eulerth  13031  pc2dvds  13129  pcz  13131  pcmpt  13142  pcmptdvds  13144  fldivp1  13147  oddprmdvds  13153  pockthg  13156  pockthi  13157  1arith  13166  zgz  13172  4sqlem19  13208  ballotfilemfmpn  13283  ballotfilemfval0  13284  ballotfilemsv  13302  ballotfilemsf1o  13306  ballotfilemrval  13310  ballotfilemro  13315  ballotfilemrinv  13326  ballotfi  13331  evenennn  13333  ennnfonelemp1  13346  ennnfonelemkh  13352  ennnfonelemnn0  13362  ssnnctlemct  13386  strslfv2  13445  strslfv  13446  basm  13463  slotm  13464  ressvalsets  13467  ressbasid  13473  qusex  13695  xpsfeq  13715  intopsn  13736  mgmidmo  13741  ismgmid  13746  mgmlrid  13748  lidrideqd  13750  lidrididd  13751  grpinvalem  13754  grpinva  13755  gzsum0  13762  issgrp  13767  imasmnd2  13808  mnd1  13811  mnd1id  13812  idmhm  13825  issubm  13828  0mhm  13842  resmhm  13843  resmhm2  13844  resmhm2b  13845  dfgrp2  13881  isgrpid2  13894  grpidd2  13895  grpinvval  13897  grpressid  13915  grpsubid1  13939  dfgrp3mlem  13952  grplactfval  13955  imasgrp2  13962  mhmlem  13966  mulgfvalg  13973  mulgnnp1  13982  mulgsubcl  13988  mulgnncl  13989  mulgnn0cl  13990  mulgcl  13991  mulgnn0z  14001  mulgneg2  14008  mulgmodid  14013  submmulg  14018  issubg  14025  subgid  14027  subgex  14028  subg0  14032  subginv  14033  subgcl  14036  subgsub  14038  subgmulg  14040  issubg3  14044  isnsg  14054  isnsg3  14059  nmzsubg  14062  nmznsg  14065  eqgval  14075  idghm  14111  resghm  14112  ghmnsgima  14120  ablressid  14188  gsum0cmn  14203  pwsval  14253  mgpvalg  14269  rngressid  14302  ringressid  14417  imasring  14418  opprvalg  14423  opprsubgg  14439  dvdsrex  14454  dvdsrtr  14457  unitinvcl  14479  unitinvinv  14480  unitlinv  14482  unitrinv  14483  opprlring  14553  issubrng  14556  subrngid  14558  issubrng2  14567  issubrg  14578  subrgid  14580  issubrg2  14598  rrgval  14619  isdomn  14627  aprprop  14650  drnggrp  14662  opprdrng  14669  lmodlema  14677  islmodd  14678  rmodislmod  14737  lsssn0  14756  sraval  14823  sraring  14835  sralmod  14836  rlmvalg  14840  rlmbasg  14841  rlmplusgg  14842  rlm0g  14843  rlmsubg  14844  rlmmulrg  14845  rlmscabas  14846  rlmvscag  14847  rlmtopng  14848  rlmdsg  14849  rlmvnegg  14851  lidlss  14862  lidlssbas  14863  lidlbas  14864  crngridl  14916  zringinvg  14988  mulgrhm  14993  znval  15020  znf1o  15035  aspval  15064  asclfval  15070  psrbagfsupp  15104  psrbaglesupp  15107  psrbaglecl  15109  psrbagcon  15111  psrelbasfun  15117  mplvalcoe  15130  tsettps  15188  baspartn  15200  eltg  15202  en1top  15227  isopn3  15275  resttopon  15321  lmbr2  15364  cnptopresti  15388  cndis  15391  lmfpm  15393  lmcl  15395  lmff  15399  txswaphmeolem  15470  ispsmet  15473  psmet0  15477  xmetunirn  15508  bl2in  15553  metrest  15656  expcn  15719  cncfmptid  15747  negcncf  15755  negfcncf  15756  hovera  15797  hoverb  15798  limccl  15809  eldvap  15832  dvexp  15861  dvmptid  15866  dveflem  15876  dvef  15877  elply  15884  plypow  15894  dvply1  15915  efap1p  15929  logge0b  16042  logle1b  16044  logfac  16048  logcxp  16052  log2tlbndlog2  16139  ppidif  16175  ppiqltx  16183  fsumdvdsmul  16186  perfectlem2  16198  bclbnd  16205  bposlem3  16211  bposlem5  16213  zabsle1  16216  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdirnn0  16264  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2dlem1  16278  2lgslem1a1  16303  2lgslem1a2  16304  2lgslem1b  16306  2lgslem1c  16307  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgsoddprmlem2  16323  2lgsoddprmlem3d  16327  edgfndxid  16348  uhgr0e  16421  umgrislfupgrdom  16470  ausgrusgrien  16510  egrsubgr  16602  uhgrsubgrself  16605  uhgrspanop  16621  clwwlkext2edg  16761  clwwlknccat  16762  clwwlknonmpo  16767  iseupth  16786  bj-ex  16888  bdth  16955  bj-indind  17056  exmidcon  17135  exmidpeirce  17136