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

Definition df-2 9624
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 9615 . 2  class  2
2 c1 8592 . . 3  class  1
3 caddc 8594 . . 3  class  +
42, 2, 3co 5685 . 2  class  ( 1  +  1 )
51, 4wceq 1608 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9635  2pos  9648  1p1e2  9660  2p2e4  9661  2times  9662  3p2e5  9674  4p2e6  9676  5p2e7  9679  6p2e8  9683  7p2e9  9686  8p2e10  9688  2nn  9696  1lt2  9705  nneo  9913  6p6e12  9993  7p5e12  9995  8p4e12  9999  9p2e11  10004  9p3e12  10005  eluz2b1  10107  x2times  10436  fztp  10656  fzprval  10659  fztpval  10660  sqval  10978  fac2  11108  faclbnd4lem1  11120  bcp1m1  11146  hashprg  11181  swrds2  11373  iseralt  11968  binom11  12101  climcndslem1  12116  climcndslem2  12117  ege2le3  12179  ef4p  12201  efgt1p2  12202  eirrlem  12290  odd2np1lem  12394  bitsfzolem  12433  bitsinv1lem  12440  isprm3  12575  prmind2  12577  opoe  12672  pockthlem  12760  pockthg  12761  prmunb  12769  prmreclem2  12772  4sqlem19  12818  vdwlem12  12847  decexp2  12898  2expltfac  12913  mulg2  14257  efgs1b  14726  efgredlemc  14735  lt6abl  14862  abvtrivd  15286  pjthlem1  18479  ovolunlem1a  18533  ovolicc1  18553  vitalilem2  18642  itgcnlem  18822  dveflem  19004  coskpi  19562  ang180lem3  19684  tanatan  19865  cosatan  19867  atantayl2  19884  emcllem7  19945  basellem3  19970  basellem5  19972  basellem8  19975  issqf  20024  ppi2  20058  ppi3  20059  cht2  20060  ppieq0  20064  ppiublem2  20092  chpeq0  20097  chtublem  20100  chtub  20101  chpub  20109  mersenne  20116  perfectlem2  20119  bcp1ctr  20168  bclbnd  20169  bposlem1  20173  bposlem2  20174  bposlem6  20178  lgslem1  20185  lgsval2lem  20195  lgsdir2lem2  20213  lgsdir2lem3  20214  lgsdirprm  20218  lgseisen  20242  m1lgs  20251  rplogsumlem1  20283  rplogsumlem2  20284  dchrisum0flb  20309  dchrisum0re  20312  mulog2sumlem2  20334  pntrmax  20363  pntpbnd2  20386  pntibndlem2  20390  pntlemg  20397  pntlemr  20401  ex-fl  20465  1p1e2apr1  20470  vc2  20742  ipval2  20911  ip2i  21037  hv2times  21271  pjhthlem1  21601  ho2times  22030  stm1addi  22456  staddi  22457  stadd3i  22459  addltmulALT  22657  subfacp1lem1  22682  subfacp1lem5  22687  subfacp1lem6  22688  vdgr1d  22866  konigsberg  22883  axlowdimlem4  23553  axlowdimlem13  23562  bpoly1  23766  bpolydiflem  23769  bpoly3  23773  bpoly4  23774  intset  25016  pell14qrgapw  25933  rmydioph  26079  rmxdioph  26081  expdiophlem1  26086  expdiophlem2  26087  expdioph  26088  psgnunilem2  26390
  Copyright terms: Public domain W3C validator