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  4175  a9evsep  4257  axnul  4260  sepab  4280  rabex2  4284  intid  4366  opm  4376  opth1  4378  opth  4379  copsex4g  4389  0nelop  4390  moop2  4394  pocl  4450  swopo  4453  limeq  4524  suceq  4549  eusvnfb  4602  onintexmid  4722  nn0eln0  4769  elvvuni  4841  coss1  4937  coss2  4938  dmxpm  5004  elrnmpt1  5035  soirri  5185  relcnvtr  5310  relssdmrn  5311  cnvpom  5333  fveqeq2  5707  fsn2g  5886  funopsn  5894  fvsng  5914  isose  6030  canth  6039  riota2f  6064  riotaeqimp  6066  acexmidlemab  6082  fvoveq1  6111  0neqopab  6136  ssoprab2  6147  caovcld  6246  caovcomd  6249  caovassd  6252  caovcand  6255  caovordid  6259  caovordd  6261  caovdid  6268  caovdird  6271  caovimo  6286  f1opw  6300  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  xpexgALT  6370  op1stg  6388  op2ndg  6389  releldm2  6423  opabn1stprc  6433  elopabi  6435  dfmpo  6463  smoeq  6566  tfr1onlemaccex  6624  tfrcllemaccex  6637  rdgisucinc  6661  rdg0g  6664  oacl  6738  nna0r  6756  nnmsucr  6766  ercnv  6833  swoord1  6841  swoord2  6842  eqer  6844  ider  6845  iinerm  6886  brecop  6904  fsetdmprc0  6955  ixpssmapg  7016  elixpsn  7023  en1bg  7093  fundmeng  7101  rex2dom  7116  xpsneng  7126  mapen  7152  phplem3g  7163  php5  7165  php5dom  7170  findcard2d  7201  findcard2sd  7202  undifdc  7237  xpfi  7245  0fsupp  7305  elfir  7312  fi0  7314  ordiso2  7381  ctssdclemr  7458  nnnninfeq2  7475  nninfisol  7479  ctssexmid  7496  nninfinfwlpo  7526  exmidaclem  7570  djuenun  7574  papeq2  7616  papirr  7617  exmidapne  7632  cc1  7637  cc2lem  7638  mulidnq  7762  ltsonq  7771  halfnqq  7783  nqnq0pi  7811  nq02m  7838  cauappcvgprlemm  8018  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  cauappcvgpr  8035  ltposr  8136  0idsr  8140  1idsr  8141  mappsrprg  8177  ax1rid  8250  ax0id  8251  axpre-ltirr  8255  mulrid  8329  1p1times  8467  cnegexlem3  8510  pncan1  8711  npcan1  8712  kcnktkm1cn  8717  apirr  8941  recexap  8989  msq0  9005  eqneg  9070  subrecap  9177  lediv2a  9233  nn1m1nn  9331  2txmxeqx  9445  subhalfhalf  9551  add1p1  9566  sub1m1  9567  cnm2m1cnm3  9568  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  nn0addcl  9609  nn0mulcl  9610  zadd2cl  9785  nn0ledivnn  10184  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xnegneg  10251  xnegid  10277  xaddid1  10280  fzss1  10485  fzssp1  10489  fzshftral  10531  0elfz  10541  nn0fz0  10542  elfz0add  10543  fz0tp  10545  elfzoelz  10570  fzoval  10571  fzoss2  10597  fzossrbm1  10598  fzouzsplit  10604  elfzo1  10619  fzonn0p1  10645  fzossfzop1  10646  fzoend  10656  fzosplitsn  10667  fvinim0ffz  10676  2tnp1ge0ge0  10756  fldiv4p1lem1div2  10760  frec2uzltd  10860  frec2uzrand  10862  uzenom  10882  frecfzennn  10883  seqeq1  10907  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqk  10964  seq3f1olemstep  10971  seq3f1olemp  10972  seq3f1oleml  10973  seqf1oglem2  10977  seq3id  10982  seq3id2  10983  ser0f  10991  m1expcl2  11018  resq01  11115  sqoddm1div8  11151  mulsubdivbinom2ap  11170  faclbnd  11200  facubnd  11204  bcpasc  11225  hashcl  11241  omgadd  11263  hashfibc  11304  snopiswrd  11335  elovmpowrd  11367  lswwrd  11372  ccatval1  11386  ccatsymb  11391  ccatass  11397  ccat1st1st  11430  swrdf  11448  pfxsuff1eqwrdeq  11492  ccatpfx  11494  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  swrdccatin2d  11537  reuccatpfxs1lem  11539  s3eq2  11570  reval  11635  imval  11636  crim  11644  replim  11645  sq01  11681  rexuz3  11777  absval  11788  sqrt0  11791  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrex  11813  abs00  11851  leabs  11861  absimle  11872  cau3  11903  dfabsmax  12005  climshft  12094  fsum3  12178  fsumcnv  12228  fsumiun  12268  binom  12275  bcxmaslem1  12279  isumshft  12281  arisum  12289  arisum2  12290  trireciplem  12291  trirecip  12292  geo2sum2  12306  geo2lim  12307  prodf1f  12334  prod0  12376  fprodfac  12406  ege2le3  12462  ef4p  12485  efgt1p2  12486  efgt1p  12487  sinval  12493  cosval  12494  negdvdsb  12598  dvdsnegb  12599  dvdsssfz1  12643  dvds1  12644  3dvds  12655  even2n  12665  oddge22np1  12672  2tp1odd  12675  ltoddhalfle  12684  m1expo  12691  m1exp1  12692  flodddiv4  12727  bits0e  12740  bits0o  12741  bitsp1e  12743  bitsp1o  12744  bitsfzo  12746  bitsinv1lem  12752  bitsinv1  12753  gcdsupex  12758  gcdsupcl  12759  alginv  12849  algcvg  12850  algcvga  12853  algfx  12854  eucalgcvga  12860  lcmdvds  12881  phimul  13032  eulerth  13039  pc2dvds  13137  pcz  13139  pcmpt  13150  pcmptdvds  13152  fldivp1  13155  oddprmdvds  13161  pockthg  13164  pockthi  13165  1arith  13174  zgz  13180  4sqlem19  13216  ballotfilemfmpn  13291  ballotfilemfval0  13292  ballotfilemsv  13310  ballotfilemsf1o  13314  ballotfilemrval  13318  ballotfilemro  13323  ballotfilemrinv  13334  ballotfi  13339  evenennn  13341  ennnfonelemp1  13354  ennnfonelemkh  13360  ennnfonelemnn0  13370  ssnnctlemct  13394  strslfv2  13453  strslfv  13454  basm  13471  slotm  13472  ressvalsets  13475  ressbasid  13482  qusex  13704  xpsfeq  13724  intopsn  13745  mgmidmo  13750  ismgmid  13755  mgmlrid  13757  lidrideqd  13759  lidrididd  13760  grpinvalem  13763  grpinva  13764  gzsum0  13771  issgrp  13776  imasmnd2  13817  mnd1  13820  mnd1id  13821  idmhm  13834  issubm  13837  0mhm  13851  resmhm  13852  resmhm2  13853  resmhm2b  13854  dfgrp2  13890  isgrpid2  13903  grpidd2  13904  grpinvval  13906  grpressid  13924  grpsubid1  13948  dfgrp3mlem  13961  grplactfval  13964  imasgrp2  13971  mhmlem  13975  mulgfvalg  13982  mulgnnp1  13991  mulgsubcl  13997  mulgnncl  13998  mulgnn0cl  13999  mulgcl  14000  mulgnn0z  14010  mulgneg2  14017  mulgmodid  14022  submmulg  14027  issubg  14034  subgid  14036  subgex  14037  subg0  14041  subginv  14042  subgcl  14045  subgsub  14047  subgmulg  14049  issubg3  14053  isnsg  14063  isnsg3  14068  nmzsubg  14071  nmznsg  14074  eqgval  14084  idghm  14120  resghm  14121  ghmnsgima  14129  cntrval  14150  cntzssv  14159  ablressid  14228  gsum0cmn  14243  pwsval  14310  mgpvalg  14326  rngressid  14359  ringressid  14476  imasring  14477  opprvalg  14482  opprsubgg  14498  dvdsrex  14513  dvdsrtr  14516  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  opprlring  14612  issubrng  14615  subrngid  14617  issubrng2  14626  issubrg  14637  subrgid  14639  issubrg2  14657  rrgval  14678  isdomn  14686  aprprop  14709  drnggrp  14721  opprdrng  14728  lmodlema  14736  islmodd  14737  rmodislmod  14796  lsssn0  14815  sraval  14882  sraring  14894  sralmod  14895  rlmvalg  14899  rlmbasg  14900  rlmplusgg  14901  rlm0g  14902  rlmsubg  14903  rlmmulrg  14904  rlmscabas  14905  rlmvscag  14906  rlmtopng  14907  rlmdsg  14908  rlmvnegg  14910  lidlss  14921  lidlssbas  14922  lidlbas  14923  crngridl  14975  zringinvg  15047  mulgrhm  15052  znval  15079  znf1o  15094  aspval  15123  asclfval  15129  psrbaglesupp  15171  psrbaglecl  15172  psrbagcon  15174  psrelbasfun  15190  mplvalg  15222  tsettps  15281  baspartn  15293  eltg  15295  en1top  15320  isopn3  15368  resttopon  15414  lmbr2  15457  cnptopresti  15481  cndis  15484  lmfpm  15486  lmcl  15488  lmff  15492  txswaphmeolem  15563  ispsmet  15566  psmet0  15570  xmetunirn  15601  bl2in  15646  metrest  15749  expcn  15812  cncfmptid  15840  negcncf  15848  negfcncf  15849  hovera  15890  hoverb  15891  limccl  15902  eldvap  15925  dvexp  15954  dvmptid  15959  dveflem  15969  dvef  15970  elply  15977  plypow  15987  dvply1  16008  efap1p  16022  logge0b  16137  logle1b  16139  logfac  16143  logcxp  16147  log2tlbndlog2  16237  chtdif  16281  ppidif  16286  ppiqltx  16298  prmorcht  16299  fsumdvdsmul  16302  chtublem  16312  chtqub  16313  perfectlem2  16317  bclbnd  16324  bposlem3  16330  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  zabsle1  16340  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdirnn0  16388  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  gausslemma2dlem1  16402  2lgslem1a1  16427  2lgslem1a2  16428  2lgslem1b  16430  2lgslem1c  16431  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgsoddprmlem2  16447  2lgsoddprmlem3d  16451  edgfndxid  16472  uhgr0e  16545  umgrislfupgrdom  16594  ausgrusgrien  16634  egrsubgr  16726  uhgrsubgrself  16729  uhgrspanop  16745  clwwlkext2edg  16885  clwwlknccat  16886  clwwlknonmpo  16891  iseupth  16910  bj-ex  17012  bdth  17079  bj-indind  17180  exmidcon  17259  exmidpeirce  17260