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 10833
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 10824 . 2 class 2
2 c1 9691 . . 3 class 1
3 caddc 9693 . . 3 class +
42, 2, 3co 6425 . 2 class (1 + 1)
51, 4wceq 1474 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  10844  0le2  10865  2pos  10866  1p1e2  10888  2p2e4  10898  2times  10899  3p2e5  10914  4p2e6  10916  5p2e7  10919  6p2e8  10923  7p2e9  10926  8p2e10OLD  10928  2nn  10939  1lt2  10948  nneo  11200  6p6e12  11341  7p5e12  11346  8p2e10  11349  8p4e12  11353  9p2e11  11358  9p2e11OLD  11359  9p3e12  11360  5t2e10  11373  eluz2b1  11498  x2times  11867  fztp  12134  fzprval  12138  fztpval  12139  fzo12sn  12285  sqval  12651  fac2  12795  faclbnd4lem1  12809  bcp1m1  12836  hashprg  12907  hashge2el2difr  12979  swrds2  13390  iseralt  14130  binom11  14270  climcndslem1  14287  climcndslem2  14288  bpoly1  14488  bpolydiflem  14491  bpoly3  14495  bpoly4  14496  ege2le3  14526  ef4p  14549  efgt1p2  14550  eirrlem  14638  odd2np1lem  14769  opoe  14792  bitsfzolem  14864  bitsfzolemOLD  14865  isprm3  15108  prmind2  15110  dvdsnprmd  15115  prmgt1  15121  pockthlem  15329  pockthg  15330  prmunb  15338  prmreclem2  15341  4sqlem19  15387  vdwlem12  15416  prmgaplem8  15482  decexp2  15499  2expltfac  15519  gsumpr12val  16995  mulg2  17263  psgnunilem2  17628  efgs1b  17878  efgredlemc  17887  lt6abl  18024  abvtrivd  18568  m2detleiblem2  20154  pjthlem1  22892  ovolunlem1a  22947  ovolicc1  22967  vitalilem2  23060  itgcnlem  23238  dveflem  23422  coskpi  23964  ang180lem3  24229  tanatan  24334  cosatan  24336  atantayl2  24353  emcllem7  24416  basellem3  24499  basellem5  24501  basellem8  24504  issqf  24552  ppi2  24586  ppi3  24587  cht2  24588  ppieq0  24592  ppiublem2  24618  chpeq0  24623  chtub  24627  chpub  24635  mersenne  24642  perfectlem2  24645  bcp1ctr  24694  bclbnd  24695  bposlem1  24699  bposlem2  24700  bposlem6  24704  lgslem1  24712  lgsval2lem  24722  lgsdir2lem2  24741  lgsdir2lem3  24742  lgsdirprm  24746  lgseisen  24794  m1lgs  24803  rplogsumlem1  24863  rplogsumlem2  24864  dchrisum0flb  24889  dchrisum0re  24892  mulog2sumlem2  24914  pntrmax  24943  pntpbnd2  24966  pntibndlem2  24970  pntlemg  24977  pntlemr  24981  axlowdimlem4  25516  axlowdimlem13  25525  constr3trllem3  25919  constr3pthlem1  25922  constr3pthlem3  25924  clwlkisclwwlklem2a  26052  vdgr1d  26169  konigsberg  26253  numclwlk2lem2f1o  26371  ex-fl  26435  1p1e2apr1  26453  vc2  26549  ipval2  26720  ip2i  26846  hv2times  27091  pjhthlem1  27423  ho2times  27851  stm1addi  28277  staddi  28278  stadd3i  28280  addltmulALT  28478  subfacp1lem1  30261  subfacp1lem5  30266  subfacp1lem6  30267  sin2h  32444  tan2h  32446  poimirlem25  32479  poimirlem27  32481  itg2addnclem3  32508  pell14qrgapw  36333  rmydioph  36474  rmxdioph  36476  expdiophlem1  36481  expdiophlem2  36482  expdioph  36483  relexp2  36870  stoweidlem14  38797  wallispilem3  38850  wallispi2lem2  38855  fourierswlem  39015  perfectALTVlem2  40060  nnsum3primes4  40099  nnsum3primesgbe  40103  fzosplitpr  40279  clwlkclwwlklem2a  41299  11wlkdlem1  41396  upgr3v3e3cycl  41439  upgr4cycl4dv4e  41444  av-numclwlk2lem2f1o  41627  difmodm1lt  42203  nnlog2ge0lt1  42250
  Copyright terms: Public domain W3C validator