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  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  3607  rabsnt  3782  unisng  3947  dfnfc2  3948  ssbr  4169  a9evsep  4250  axnul  4253  sepab  4273  rabex2  4277  intid  4359  opm  4369  opth1  4371  opth  4372  copsex4g  4382  0nelop  4383  moop2  4387  pocl  4443  swopo  4446  limeq  4517  suceq  4542  eusvnfb  4595  onintexmid  4715  nn0eln0  4762  elvvuni  4834  coss1  4930  coss2  4931  dmxpm  4997  elrnmpt1  5028  soirri  5177  relcnvtr  5302  relssdmrn  5303  cnvpom  5325  fveqeq2  5699  fsn2g  5874  funopsn  5882  fvsng  5902  isose  6017  canth  6026  riota2f  6051  riotaeqimp  6053  acexmidlemab  6069  fvoveq1  6098  0neqopab  6123  ssoprab2  6134  caovcld  6233  caovcomd  6236  caovassd  6239  caovcand  6242  caovordid  6246  caovordd  6248  caovdid  6255  caovdird  6258  caovimo  6273  f1opw  6287  caofref  6317  caofinvl  6318  caofid0l  6319  caofid0r  6320  xpexgALT  6356  op1stg  6374  op2ndg  6375  releldm2  6409  opabn1stprc  6419  elopabi  6421  dfmpo  6449  smoeq  6551  tfr1onlemaccex  6609  tfrcllemaccex  6622  rdgisucinc  6646  rdg0g  6649  oacl  6723  nna0r  6741  nnmsucr  6751  ercnv  6818  swoord1  6826  swoord2  6827  eqer  6829  ider  6830  iinerm  6871  brecop  6889  fsetdmprc0  6940  ixpssmapg  7000  elixpsn  7007  en1bg  7077  fundmeng  7085  rex2dom  7100  xpsneng  7110  mapen  7136  phplem3g  7147  php5  7149  php5dom  7154  findcard2d  7185  findcard2sd  7186  undifdc  7221  xpfi  7229  fsuppxpfi  7286  elfir  7297  fi0  7299  ordiso2  7365  ctssdclemr  7442  nnnninfeq2  7459  nninfisol  7463  ctssexmid  7480  nninfinfwlpo  7510  exmidaclem  7554  djuenun  7558  papeq2  7600  papirr  7601  exmidapne  7616  cc1  7621  cc2lem  7622  mulidnq  7746  ltsonq  7755  halfnqq  7767  nqnq0pi  7795  nq02m  7822  cauappcvgprlemm  8002  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem2  8017  cauappcvgpr  8019  ltposr  8120  0idsr  8124  1idsr  8125  mappsrprg  8161  ax1rid  8234  ax0id  8235  axpre-ltirr  8239  mulrid  8313  1p1times  8450  cnegexlem3  8493  pncan1  8694  npcan1  8695  kcnktkm1cn  8700  apirr  8923  recexap  8971  msq0  8987  eqneg  9052  subrecap  9159  lediv2a  9215  nn1m1nn  9301  2txmxeqx  9415  subhalfhalf  9519  add1p1  9534  sub1m1  9535  cnm2m1cnm3  9536  xp1d2m1eqxm1d2  9537  div4p1lem1div2  9538  nn0addcl  9577  nn0mulcl  9578  zadd2cl  9754  nn0ledivnn  10147  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xnegneg  10214  xnegid  10240  xaddid1  10243  fzss1  10447  fzssp1  10451  fzshftral  10493  0elfz  10503  nn0fz0  10504  elfz0add  10505  fz0tp  10507  elfzoelz  10532  fzoval  10533  fzoss2  10559  fzossrbm1  10560  fzouzsplit  10566  elfzo1  10581  fzonn0p1  10607  fzossfzop1  10608  fzoend  10618  fzosplitsn  10629  fvinim0ffz  10638  2tnp1ge0ge0  10714  fldiv4p1lem1div2  10718  frec2uzltd  10818  frec2uzrand  10820  uzenom  10840  frecfzennn  10841  seqeq1  10865  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqk  10922  seq3f1olemstep  10929  seq3f1olemp  10930  seq3f1oleml  10931  seqf1oglem2  10935  seq3id  10940  seq3id2  10941  ser0f  10949  m1expcl2  10976  resq01  11073  sqoddm1div8  11109  mulsubdivbinom2ap  11127  faclbnd  11157  facubnd  11161  bcpasc  11182  hashcl  11198  omgadd  11220  hashfibc  11261  snopiswrd  11292  elovmpowrd  11324  lswwrd  11329  ccatval1  11343  ccatsymb  11348  ccatass  11354  ccat1st1st  11387  swrdf  11405  pfxsuff1eqwrdeq  11449  ccatpfx  11451  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccatin2d  11494  reuccatpfxs1lem  11496  s3eq2  11527  reval  11592  imval  11593  crim  11601  replim  11602  sq01  11638  rexuz3  11734  absval  11745  sqrt0  11748  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrex  11770  abs00  11808  leabs  11818  absimle  11828  cau3  11859  dfabsmax  11961  climshft  12048  fsum3  12132  fsumcnv  12182  fsumiun  12222  binom  12229  bcxmaslem1  12233  isumshft  12235  arisum  12243  arisum2  12244  trireciplem  12245  trirecip  12246  geo2sum2  12260  geo2lim  12261  prodf1f  12288  prod0  12330  fprodfac  12360  ege2le3  12416  ef4p  12439  efgt1p2  12440  efgt1p  12441  sinval  12447  cosval  12448  negdvdsb  12552  dvdsnegb  12553  dvdsssfz1  12597  dvds1  12598  3dvds  12609  even2n  12619  oddge22np1  12626  2tp1odd  12629  ltoddhalfle  12638  m1expo  12645  m1exp1  12646  flodddiv4  12681  bits0e  12694  bits0o  12695  bitsp1e  12697  bitsp1o  12698  bitsfzo  12700  bitsinv1lem  12706  bitsinv1  12707  gcdsupex  12712  gcdsupcl  12713  alginv  12803  algcvg  12804  algcvga  12807  algfx  12808  eucalgcvga  12814  lcmdvds  12835  pw2dvds  12922  oddpwdclemodd  12928  phimul  12982  eulerth  12989  pc2dvds  13087  pcz  13089  pcmpt  13100  pcmptdvds  13102  fldivp1  13105  oddprmdvds  13111  pockthg  13114  pockthi  13115  1arith  13124  zgz  13130  4sqlem19  13166  ballotfilemfmpn  13212  ballotfilemfval0  13213  ballotfilemsv  13231  ballotfilemsf1o  13235  ballotfilemrval  13239  ballotfilemro  13244  ballotfilemrinv  13255  ballotfi  13260  evenennn  13262  ennnfonelemp1  13275  ennnfonelemkh  13281  ennnfonelemnn0  13291  ssnnctlemct  13315  strslfv2  13374  strslfv  13375  basm  13392  ressvalsets  13395  ressbasid  13401  qusex  13623  xpsfeq  13643  intopsn  13664  mgmidmo  13669  ismgmid  13674  mgmlrid  13676  lidrideqd  13678  lidrididd  13679  grpinvalem  13682  grpinva  13683  gzsum0  13690  issgrp  13695  imasmnd2  13736  mnd1  13739  mnd1id  13740  idmhm  13753  issubm  13756  0mhm  13770  resmhm  13771  resmhm2  13772  resmhm2b  13773  dfgrp2  13809  isgrpid2  13822  grpidd2  13823  grpinvval  13825  grpressid  13843  grpsubid1  13867  dfgrp3mlem  13880  grplactfval  13883  imasgrp2  13890  mhmlem  13894  mulgfvalg  13901  mulgnnp1  13910  mulgsubcl  13916  mulgnncl  13917  mulgnn0cl  13918  mulgcl  13919  mulgnn0z  13929  mulgneg2  13936  mulgmodid  13941  submmulg  13946  issubg  13953  subgid  13955  subgex  13956  subg0  13960  subginv  13961  subgcl  13964  subgsub  13966  subgmulg  13968  issubg3  13972  isnsg  13982  isnsg3  13987  nmzsubg  13990  nmznsg  13993  eqgval  14003  idghm  14039  resghm  14040  ghmnsgima  14048  ablressid  14116  gsum0cmn  14131  pwsval  14181  mgpvalg  14197  rngressid  14228  ringressid  14341  imasring  14342  opprvalg  14347  opprsubgg  14363  dvdsrex  14378  dvdsrtr  14381  unitinvcl  14403  unitinvinv  14404  unitlinv  14406  unitrinv  14407  opprlring  14477  issubrng  14480  subrngid  14482  issubrng2  14491  issubrg  14502  subrgid  14504  issubrg2  14522  rrgval  14543  isdomn  14551  aprprop  14574  drnggrp  14586  opprdrng  14593  lmodlema  14601  islmodd  14602  rmodislmod  14660  lsssn0  14679  sraval  14746  sraring  14758  sralmod  14759  rlmvalg  14763  rlmbasg  14764  rlmplusgg  14765  rlm0g  14766  rlmsubg  14767  rlmmulrg  14768  rlmscabas  14769  rlmvscag  14770  rlmtopng  14771  rlmdsg  14772  rlmvnegg  14774  lidlss  14785  lidlssbas  14786  lidlbas  14787  crngridl  14839  zringinvg  14911  mulgrhm  14916  znval  14943  znf1o  14958  psrbagfsupp  14978  psrbaglesupp  14981  psrbaglecl  14983  psrbagcon  14985  psrelbasfun  14991  mplvalcoe  15004  tsettps  15062  baspartn  15074  eltg  15076  en1top  15101  isopn3  15149  resttopon  15195  lmbr2  15238  cnptopresti  15262  cndis  15265  lmfpm  15267  lmcl  15269  lmff  15273  txswaphmeolem  15344  ispsmet  15347  psmet0  15351  xmetunirn  15382  bl2in  15427  metrest  15530  expcn  15593  cncfmptid  15621  negcncf  15629  negfcncf  15630  hovera  15671  hoverb  15672  limccl  15683  eldvap  15706  dvexp  15735  dvmptid  15740  dveflem  15750  dvef  15751  elply  15758  plypow  15768  dvply1  15789  logge0b  15914  logle1b  15916  logfac  15918  logcxp  15922  fsumdvdsmul  16019  perfectlem2  16028  zabsle1  16032  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsdir2lem2  16062  lgsdir2lem4  16064  lgsdirnn0  16080  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  gausslemma2dlem1  16094  2lgslem1a1  16119  2lgslem1a2  16120  2lgslem1b  16122  2lgslem1c  16123  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgsoddprmlem2  16139  2lgsoddprmlem3d  16143  edgfndxid  16164  uhgr0e  16237  umgrislfupgrdom  16286  ausgrusgrien  16326  egrsubgr  16418  uhgrsubgrself  16421  uhgrspanop  16437  clwwlkext2edg  16577  clwwlknccat  16578  clwwlknonmpo  16583  iseupth  16602  bj-ex  16704  bdth  16771  bj-indind  16872  exmidcon  16950  exmidpeirce  16951