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 10956
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 10947 . 2 class 2
2 c1 9816 . . 3 class 1
3 caddc 9818 . . 3 class +
42, 2, 3co 6549 . 2 class (1 + 1)
51, 4wceq 1475 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  10967  0le2  10988  2pos  10989  1p1e2  11011  2p2e4  11021  2times  11022  3p2e5  11037  4p2e6  11039  5p2e7  11042  6p2e8  11046  7p2e9  11049  8p2e10OLD  11051  2nn  11062  1lt2  11071  nneo  11337  6p6e12  11478  7p5e12  11483  8p2e10  11486  8p4e12  11490  9p2e11  11495  9p2e11OLD  11496  9p3e12  11497  5t2e10  11510  eluz2b1  11635  x2times  12001  fztp  12267  fzprval  12271  fztpval  12272  fzo12sn  12418  sqval  12784  fac2  12928  faclbnd4lem1  12942  bcp1m1  12969  hashprg  13043  hashprgOLD  13044  hashge2el2difr  13118  swrds2  13533  iseralt  14263  binom11  14403  climcndslem1  14420  climcndslem2  14421  bpoly1  14621  bpolydiflem  14624  bpoly3  14628  bpoly4  14629  ege2le3  14659  ef4p  14682  efgt1p2  14683  eirrlem  14771  odd2np1lem  14902  opoe  14925  bitsfzolem  14994  isprm3  15234  prmind2  15236  dvdsnprmd  15241  prmgt1  15247  pockthlem  15447  pockthg  15448  prmunb  15456  prmreclem2  15459  4sqlem19  15505  vdwlem12  15534  prmgaplem8  15600  decexp2  15617  2expltfac  15637  gsumpr12val  17105  mulg2  17373  psgnunilem2  17738  efgs1b  17972  efgredlemc  17981  lt6abl  18119  abvtrivd  18663  m2detleiblem2  20253  clmvs2  22702  cphipval  22850  pjthlem1  23016  ovolunlem1a  23071  ovolicc1  23091  vitalilem2  23184  itgcnlem  23362  dveflem  23546  coskpi  24076  ang180lem3  24341  tanatan  24446  cosatan  24448  atantayl2  24465  emcllem7  24528  basellem3  24609  basellem5  24611  basellem8  24614  issqf  24662  ppi2  24696  ppi3  24697  cht2  24698  ppieq0  24702  ppiublem2  24728  chpeq0  24733  chtub  24737  chpub  24745  mersenne  24752  perfectlem2  24755  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  bposlem2  24810  bposlem6  24814  lgslem1  24822  lgsval2lem  24832  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsdirprm  24856  lgseisen  24904  m1lgs  24913  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0flb  24999  dchrisum0re  25002  mulog2sumlem2  25024  pntrmax  25053  pntpbnd2  25076  pntibndlem2  25080  pntlemg  25087  pntlemr  25091  axlowdimlem4  25625  axlowdimlem13  25634  constr3trllem3  26180  constr3pthlem1  26183  constr3pthlem3  26185  clwlkisclwwlklem2a  26313  vdgr1d  26430  konigsberg  26514  numclwlk2lem2f1o  26632  ex-fl  26696  1p1e2apr1  26714  vc2OLD  26807  ipval2  26946  ip2i  27067  hv2times  27302  pjhthlem1  27634  ho2times  28062  stm1addi  28488  staddi  28489  stadd3i  28491  addltmulALT  28689  subfacp1lem1  30415  subfacp1lem5  30420  subfacp1lem6  30421  sin2h  32569  tan2h  32571  poimirlem25  32604  poimirlem27  32606  itg2addnclem3  32633  pell14qrgapw  36458  rmydioph  36599  rmxdioph  36601  expdiophlem1  36606  expdiophlem2  36607  expdioph  36608  relexp2  36988  stoweidlem14  38907  wallispilem3  38960  wallispi2lem2  38965  fourierswlem  39123  perfectALTVlem2  40165  nnsum3primes4  40204  nnsum3primesgbe  40208  fzosplitpr  40362  clwlkclwwlklem2a  41207  11wlkdlem1  41304  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  av-numclwlk2lem2f1o  41535  difmodm1lt  42111  nnlog2ge0lt1  42158
  Copyright terms: Public domain W3C validator