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  14295  mgpvalg  14311  rngressid  14344  ringressid  14459  imasring  14460  opprvalg  14465  opprsubgg  14481  dvdsrex  14496  dvdsrtr  14499  unitinvcl  14521  unitinvinv  14522  unitlinv  14524  unitrinv  14525  opprlring  14595  issubrng  14598  subrngid  14600  issubrng2  14609  issubrg  14620  subrgid  14622  issubrg2  14640  rrgval  14661  isdomn  14669  aprprop  14692  drnggrp  14704  opprdrng  14711  lmodlema  14719  islmodd  14720  rmodislmod  14779  lsssn0  14798  sraval  14865  sraring  14877  sralmod  14878  rlmvalg  14882  rlmbasg  14883  rlmplusgg  14884  rlm0g  14885  rlmsubg  14886  rlmmulrg  14887  rlmscabas  14888  rlmvscag  14889  rlmtopng  14890  rlmdsg  14891  rlmvnegg  14893  lidlss  14904  lidlssbas  14905  lidlbas  14906  crngridl  14958  zringinvg  15030  mulgrhm  15035  znval  15062  znf1o  15077  aspval  15106  asclfval  15112  psrbagfsupp  15146  psrbaglesupp  15149  psrbaglecl  15151  psrbagcon  15153  psrelbasfun  15160  mplvalcoe  15180  tsettps  15238  baspartn  15250  eltg  15252  en1top  15277  isopn3  15325  resttopon  15371  lmbr2  15414  cnptopresti  15438  cndis  15441  lmfpm  15443  lmcl  15445  lmff  15449  txswaphmeolem  15520  ispsmet  15523  psmet0  15527  xmetunirn  15558  bl2in  15603  metrest  15706  expcn  15769  cncfmptid  15797  negcncf  15805  negfcncf  15806  hovera  15847  hoverb  15848  limccl  15859  eldvap  15882  dvexp  15911  dvmptid  15916  dveflem  15926  dvef  15927  elply  15934  plypow  15944  dvply1  15965  efap1p  15979  logge0b  16094  logle1b  16096  logfac  16100  logcxp  16104  log2tlbndlog2  16194  chtdif  16238  ppidif  16243  ppiqltx  16255  prmorcht  16256  fsumdvdsmul  16259  chtublem  16269  chtqub  16270  perfectlem2  16274  bclbnd  16281  bposlem3  16287  bposlem5  16289  bposlem6  16290  bposlem7  16291  bposlem8  16292  bposlem9  16293  zabsle1  16297  lgsval  16302  lgsfvalg  16303  lgsval2lem  16308  lgsdir2lem2  16327  lgsdir2lem4  16329  lgsdirnn0  16345  gausslemma2dlem0i  16355  gausslemma2dlem1a  16356  gausslemma2dlem1  16359  2lgslem1a1  16384  2lgslem1a2  16385  2lgslem1b  16387  2lgslem1c  16388  2lgslem3a  16391  2lgslem3b  16392  2lgslem3c  16393  2lgslem3d  16394  2lgsoddprmlem2  16404  2lgsoddprmlem3d  16408  edgfndxid  16429  uhgr0e  16502  umgrislfupgrdom  16551  ausgrusgrien  16591  egrsubgr  16683  uhgrsubgrself  16686  uhgrspanop  16702  clwwlkext2edg  16842  clwwlknccat  16843  clwwlknonmpo  16848  iseupth  16867  bj-ex  16969  bdth  17036  bj-indind  17137  exmidcon  17216  exmidpeirce  17217