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 10926
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 10917 . 2 class 2
2 c1 9793 . . 3 class 1
3 caddc 9795 . . 3 class +
42, 2, 3co 6527 . 2 class (1 + 1)
51, 4wceq 1474 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  10937  0le2  10958  2pos  10959  1p1e2  10981  2p2e4  10991  2times  10992  3p2e5  11007  4p2e6  11009  5p2e7  11012  6p2e8  11016  7p2e9  11019  8p2e10OLD  11021  2nn  11032  1lt2  11041  nneo  11293  6p6e12  11434  7p5e12  11439  8p2e10  11442  8p4e12  11446  9p2e11  11451  9p2e11OLD  11452  9p3e12  11453  5t2e10  11466  eluz2b1  11591  x2times  11958  fztp  12222  fzprval  12226  fztpval  12227  fzo12sn  12373  sqval  12739  fac2  12883  faclbnd4lem1  12897  bcp1m1  12924  hashprg  12995  hashprgOLD  12996  hashge2el2difr  13068  swrds2  13479  iseralt  14209  binom11  14349  climcndslem1  14366  climcndslem2  14367  bpoly1  14567  bpolydiflem  14570  bpoly3  14574  bpoly4  14575  ege2le3  14605  ef4p  14628  efgt1p2  14629  eirrlem  14717  odd2np1lem  14848  opoe  14871  bitsfzolem  14940  isprm3  15180  prmind2  15182  dvdsnprmd  15187  prmgt1  15193  pockthlem  15393  pockthg  15394  prmunb  15402  prmreclem2  15405  4sqlem19  15451  vdwlem12  15480  prmgaplem8  15546  decexp2  15563  2expltfac  15583  gsumpr12val  17051  mulg2  17319  psgnunilem2  17684  efgs1b  17918  efgredlemc  17927  lt6abl  18065  abvtrivd  18609  m2detleiblem2  20195  clmvs2  22633  pjthlem1  22933  ovolunlem1a  22988  ovolicc1  23008  vitalilem2  23101  itgcnlem  23279  dveflem  23463  coskpi  23993  ang180lem3  24258  tanatan  24363  cosatan  24365  atantayl2  24382  emcllem7  24445  basellem3  24526  basellem5  24528  basellem8  24531  issqf  24579  ppi2  24613  ppi3  24614  cht2  24615  ppieq0  24619  ppiublem2  24645  chpeq0  24650  chtub  24654  chpub  24662  mersenne  24669  perfectlem2  24672  bcp1ctr  24721  bclbnd  24722  bposlem1  24726  bposlem2  24727  bposlem6  24731  lgslem1  24739  lgsval2lem  24749  lgsdir2lem2  24768  lgsdir2lem3  24769  lgsdirprm  24773  lgseisen  24821  m1lgs  24830  rplogsumlem1  24890  rplogsumlem2  24891  dchrisum0flb  24916  dchrisum0re  24919  mulog2sumlem2  24941  pntrmax  24970  pntpbnd2  24993  pntibndlem2  24997  pntlemg  25004  pntlemr  25008  axlowdimlem4  25543  axlowdimlem13  25552  constr3trllem3  25946  constr3pthlem1  25949  constr3pthlem3  25951  clwlkisclwwlklem2a  26079  vdgr1d  26196  konigsberg  26280  numclwlk2lem2f1o  26398  ex-fl  26462  1p1e2apr1  26480  vc2OLD  26576  ipval2  26747  ip2i  26873  hv2times  27108  pjhthlem1  27440  ho2times  27868  stm1addi  28294  staddi  28295  stadd3i  28297  addltmulALT  28495  subfacp1lem1  30221  subfacp1lem5  30226  subfacp1lem6  30227  sin2h  32365  tan2h  32367  poimirlem25  32400  poimirlem27  32402  itg2addnclem3  32429  pell14qrgapw  36254  rmydioph  36395  rmxdioph  36397  expdiophlem1  36402  expdiophlem2  36403  expdioph  36404  relexp2  36784  stoweidlem14  38704  wallispilem3  38757  wallispi2lem2  38762  fourierswlem  38920  perfectALTVlem2  39963  nnsum3primes4  40002  nnsum3primesgbe  40006  fzosplitpr  40182  clwlkclwwlklem2a  41202  11wlkdlem1  41299  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  av-numclwlk2lem2f1o  41530  difmodm1lt  42106  nnlog2ge0lt1  42153
  Copyright terms: Public domain W3C validator