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  7376  ctssdclemr  7453  nnnninfeq2  7470  nninfisol  7474  ctssexmid  7491  nninfinfwlpo  7521  exmidaclem  7565  djuenun  7569  papeq2  7611  papirr  7612  exmidapne  7627  cc1  7632  cc2lem  7633  mulidnq  7757  ltsonq  7766  halfnqq  7778  nqnq0pi  7806  nq02m  7833  cauappcvgprlemm  8013  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  cauappcvgpr  8030  ltposr  8131  0idsr  8135  1idsr  8136  mappsrprg  8172  ax1rid  8245  ax0id  8246  axpre-ltirr  8250  mulrid  8324  1p1times  8462  cnegexlem3  8505  pncan1  8706  npcan1  8707  kcnktkm1cn  8712  apirr  8936  recexap  8984  msq0  9000  eqneg  9065  subrecap  9172  lediv2a  9228  nn1m1nn  9325  2txmxeqx  9439  subhalfhalf  9545  add1p1  9560  sub1m1  9561  cnm2m1cnm3  9562  xp1d2m1eqxm1d2  9563  div4p1lem1div2  9564  nn0addcl  9603  nn0mulcl  9604  zadd2cl  9780  nn0ledivnn  10179  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xnegneg  10246  xnegid  10272  xaddid1  10275  fzss1  10480  fzssp1  10484  fzshftral  10526  0elfz  10536  nn0fz0  10537  elfz0add  10538  fz0tp  10540  elfzoelz  10565  fzoval  10566  fzoss2  10592  fzossrbm1  10593  fzouzsplit  10599  elfzo1  10614  fzonn0p1  10640  fzossfzop1  10641  fzoend  10651  fzosplitsn  10662  fvinim0ffz  10671  2tnp1ge0ge0  10751  fldiv4p1lem1div2  10755  frec2uzltd  10855  frec2uzrand  10857  uzenom  10877  frecfzennn  10878  seqeq1  10902  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqk  10959  seq3f1olemstep  10966  seq3f1olemp  10967  seq3f1oleml  10968  seqf1oglem2  10972  seq3id  10977  seq3id2  10978  ser0f  10986  m1expcl2  11013  resq01  11110  sqoddm1div8  11146  mulsubdivbinom2ap  11165  faclbnd  11195  facubnd  11199  bcpasc  11220  hashcl  11236  omgadd  11258  hashfibc  11299  snopiswrd  11330  elovmpowrd  11362  lswwrd  11367  ccatval1  11381  ccatsymb  11386  ccatass  11392  ccat1st1st  11425  swrdf  11443  pfxsuff1eqwrdeq  11487  ccatpfx  11489  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  swrdccatin2d  11532  reuccatpfxs1lem  11534  s3eq2  11565  reval  11630  imval  11631  crim  11639  replim  11640  sq01  11676  rexuz3  11772  absval  11783  sqrt0  11786  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrex  11808  abs00  11846  leabs  11856  absimle  11867  cau3  11898  dfabsmax  12000  climshft  12089  fsum3  12173  fsumcnv  12223  fsumiun  12263  binom  12270  bcxmaslem1  12274  isumshft  12276  arisum  12284  arisum2  12285  trireciplem  12286  trirecip  12287  geo2sum2  12301  geo2lim  12302  prodf1f  12329  prod0  12371  fprodfac  12401  ege2le3  12457  ef4p  12480  efgt1p2  12481  efgt1p  12482  sinval  12488  cosval  12489  negdvdsb  12593  dvdsnegb  12594  dvdsssfz1  12638  dvds1  12639  3dvds  12650  even2n  12660  oddge22np1  12667  2tp1odd  12670  ltoddhalfle  12679  m1expo  12686  m1exp1  12687  flodddiv4  12722  bits0e  12735  bits0o  12736  bitsp1e  12738  bitsp1o  12739  bitsfzo  12741  bitsinv1lem  12747  bitsinv1  12748  gcdsupex  12753  gcdsupcl  12754  alginv  12844  algcvg  12845  algcvga  12848  algfx  12849  eucalgcvga  12855  lcmdvds  12876  phimul  13027  eulerth  13034  pc2dvds  13132  pcz  13134  pcmpt  13145  pcmptdvds  13147  fldivp1  13150  oddprmdvds  13156  pockthg  13159  pockthi  13160  1arith  13169  zgz  13175  4sqlem19  13211  ballotfilemfmpn  13286  ballotfilemfval0  13287  ballotfilemsv  13305  ballotfilemsf1o  13309  ballotfilemrval  13313  ballotfilemro  13318  ballotfilemrinv  13329  ballotfi  13334  evenennn  13336  ennnfonelemp1  13349  ennnfonelemkh  13355  ennnfonelemnn0  13365  ssnnctlemct  13389  strslfv2  13448  strslfv  13449  basm  13466  slotm  13467  ressvalsets  13470  ressbasid  13477  qusex  13699  xpsfeq  13719  intopsn  13740  mgmidmo  13745  ismgmid  13750  mgmlrid  13752  lidrideqd  13754  lidrididd  13755  grpinvalem  13758  grpinva  13759  gzsum0  13766  issgrp  13771  imasmnd2  13812  mnd1  13815  mnd1id  13816  idmhm  13829  issubm  13832  0mhm  13846  resmhm  13847  resmhm2  13848  resmhm2b  13849  dfgrp2  13885  isgrpid2  13898  grpidd2  13899  grpinvval  13901  grpressid  13919  grpsubid1  13943  dfgrp3mlem  13956  grplactfval  13959  imasgrp2  13966  mhmlem  13970  mulgfvalg  13977  mulgnnp1  13986  mulgsubcl  13992  mulgnncl  13993  mulgnn0cl  13994  mulgcl  13995  mulgnn0z  14005  mulgneg2  14012  mulgmodid  14017  submmulg  14022  issubg  14029  subgid  14031  subgex  14032  subg0  14036  subginv  14037  subgcl  14040  subgsub  14042  subgmulg  14044  issubg3  14048  isnsg  14058  isnsg3  14063  nmzsubg  14066  nmznsg  14069  eqgval  14079  idghm  14115  resghm  14116  ghmnsgima  14124  cntrval  14145  cntzssv  14154  ablressid  14223  gsum0cmn  14238  pwsval  14288  mgpvalg  14304  rngressid  14337  ringressid  14452  imasring  14453  opprvalg  14458  opprsubgg  14474  dvdsrex  14489  dvdsrtr  14492  unitinvcl  14514  unitinvinv  14515  unitlinv  14517  unitrinv  14518  opprlring  14588  issubrng  14591  subrngid  14593  issubrng2  14602  issubrg  14613  subrgid  14615  issubrg2  14633  rrgval  14654  isdomn  14662  aprprop  14685  drnggrp  14697  opprdrng  14704  lmodlema  14712  islmodd  14713  rmodislmod  14772  lsssn0  14791  sraval  14858  sraring  14870  sralmod  14871  rlmvalg  14875  rlmbasg  14876  rlmplusgg  14877  rlm0g  14878  rlmsubg  14879  rlmmulrg  14880  rlmscabas  14881  rlmvscag  14882  rlmtopng  14883  rlmdsg  14884  rlmvnegg  14886  lidlss  14897  lidlssbas  14898  lidlbas  14899  crngridl  14951  zringinvg  15023  mulgrhm  15028  znval  15055  znf1o  15070  aspval  15099  asclfval  15105  psrbagfsupp  15139  psrbaglesupp  15142  psrbaglecl  15144  psrbagcon  15146  psrelbasfun  15153  mplvalcoe  15172  tsettps  15230  baspartn  15242  eltg  15244  en1top  15269  isopn3  15317  resttopon  15363  lmbr2  15406  cnptopresti  15430  cndis  15433  lmfpm  15435  lmcl  15437  lmff  15441  txswaphmeolem  15512  ispsmet  15515  psmet0  15519  xmetunirn  15550  bl2in  15595  metrest  15698  expcn  15761  cncfmptid  15789  negcncf  15797  negfcncf  15798  hovera  15839  hoverb  15840  limccl  15851  eldvap  15874  dvexp  15903  dvmptid  15908  dveflem  15918  dvef  15919  elply  15926  plypow  15936  dvply1  15957  efap1p  15971  logge0b  16084  logle1b  16086  logfac  16090  logcxp  16094  log2tlbndlog2  16181  chtdif  16225  ppidif  16230  ppiqltx  16242  prmorcht  16243  fsumdvdsmul  16246  chtublem  16256  chtqub  16257  perfectlem2  16261  bclbnd  16268  bposlem3  16274  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  zabsle1  16284  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsdir2lem2  16314  lgsdir2lem4  16316  lgsdirnn0  16332  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  gausslemma2dlem1  16346  2lgslem1a1  16371  2lgslem1a2  16372  2lgslem1b  16374  2lgslem1c  16375  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgsoddprmlem2  16391  2lgsoddprmlem3d  16395  edgfndxid  16416  uhgr0e  16489  umgrislfupgrdom  16538  ausgrusgrien  16578  egrsubgr  16670  uhgrsubgrself  16673  uhgrspanop  16689  clwwlkext2edg  16829  clwwlknccat  16830  clwwlknonmpo  16835  iseupth  16854  bj-ex  16956  bdth  17023  bj-indind  17124  exmidcon  17203  exmidpeirce  17204