MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2 Structured version   Visualization version   GIF version

Definition df-2 11689
Description: Define the number 2. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-2 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 11681 . 2 class 2
2 c1 10527 . . 3 class 1
3 caddc 10529 . . 3 class +
42, 2, 3co 7145 . 2 class (1 + 1)
51, 4wceq 1528 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2nn  11699  2re  11700  2cn  11701  0le2  11728  2pos  11729  1p1e2  11751  2p2e4  11761  2times  11762  1p2e3  11769  3p2e5  11777  4p2e6  11779  5p2e7  11782  6p2e8  11785  7p2e9  11787  1lt2  11797  nneo  12055  6p6e12  12161  7p5e12  12164  8p2e10  12167  8p4e12  12169  9p2e11  12174  9p3e12  12175  5t2e10  12187  eluz2b1  12308  x2times  12682  fztp  12953  fz12pr  12954  fztpval  12959  fzo12sn  13110  fzosplitpr  13136  sqval  13471  fac2  13629  faclbnd4lem1  13643  bcp1m1  13670  hashprg  13746  hashgt23el  13775  hashge2el2difr  13829  swrds2  14292  iseralt  15031  binom11  15177  climcndslem1  15194  climcndslem2  15195  bpoly1  15395  bpolydiflem  15398  bpoly3  15402  bpoly4  15403  ege2le3  15433  ef4p  15456  efgt1p2  15457  eirrlem  15547  odd2np1lem  15679  opoe  15702  bitsfzolem  15773  isprm3  16017  prmind2  16019  dvdsnprmd  16024  2mulprm  16027  pockthlem  16231  pockthg  16232  prmunb  16240  prmreclem2  16243  4sqlem19  16289  vdwlem12  16318  prmgaplem8  16384  decexp2  16401  2expltfac  16416  gsumpr12val  17889  mulg2  18177  psgnunilem2  18554  efgs1b  18793  efgredlemc  18802  lt6abl  18946  abvtrivd  19542  m2detleiblem2  21167  clmvs2  23627  cphipval  23775  pjthlem1  23969  ovolunlem1a  24026  ovolicc1  24046  vitalilem2  24139  itgcnlem  24319  dveflem  24505  coskpi  25037  ang180lem3  25316  tanatan  25424  cosatan  25426  atantayl2  25443  emcllem7  25507  basellem3  25588  basellem5  25590  basellem8  25593  issqf  25641  ppi2  25675  ppi3  25676  cht2  25677  ppieq0  25681  ppiublem2  25707  chpeq0  25712  chtub  25716  chpub  25724  mersenne  25731  perfectlem2  25734  bcp1ctr  25783  bclbnd  25784  bposlem1  25788  bposlem2  25789  bposlem6  25793  lgslem1  25801  lgsval2lem  25811  lgsdir2lem2  25830  lgsdir2lem3  25831  lgsdirprm  25835  lgseisen  25883  m1lgs  25892  rplogsumlem1  25988  rplogsumlem2  25989  dchrisum0flb  26014  dchrisum0re  26017  mulog2sumlem2  26039  pntrmax  26068  pntpbnd2  26091  pntibndlem2  26095  pntlemg  26102  pntlemr  26106  axlowdimlem13  26668  clwlkclwwlklem2a  27704  1wlkdlem1  27844  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  numclwlk2lem2f1o  28086  ex-fl  28154  1p1e2apr1  28173  vc2OLD  28273  ipval2  28412  ip2i  28533  hv2times  28766  pjhthlem1  29096  ho2times  29524  stm1addi  29950  staddi  29951  stadd3i  29953  addltmulALT  30151  threehalves  30519  usgrgt2cycl  32275  subfacp1lem1  32324  subfacp1lem5  32329  subfacp1lem6  32330  sin2h  34764  tan2h  34766  poimirlem25  34799  poimirlem27  34801  itg2addnclem3  34827  sn-1ne2  39038  remul02  39115  3cubeslem3r  39164  pell14qrgapw  39353  rmydioph  39491  rmxdioph  39493  expdiophlem1  39498  expdiophlem2  39499  expdioph  39500  relexp2  39902  stoweidlem14  42180  wallispilem3  42233  wallispi2lem2  42238  fourierswlem  42396  perfectALTVlem2  43734  sbgoldbo  43799  nnsum3primes4  43800  nnsum3primesgbe  43804  difmodm1lt  44480  nnlog2ge0lt1  44524
  Copyright terms: Public domain W3C validator