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

Definition df-2 9804
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 9795 . 2  class  2
2 c1 8738 . . 3  class  1
3 caddc 8740 . . 3  class  +
42, 2, 3co 5858 . 2  class  ( 1  +  1 )
51, 4wceq 1623 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9815  2pos  9828  1p1e2  9840  2p2e4  9842  2times  9843  3p2e5  9855  4p2e6  9857  5p2e7  9860  6p2e8  9864  7p2e9  9867  8p2e10  9869  2nn  9877  1lt2  9886  nneo  10095  6p6e12  10175  7p5e12  10177  8p4e12  10181  9p2e11  10186  9p3e12  10187  eluz2b1  10289  x2times  10619  fztp  10841  fzprval  10844  fztpval  10845  sqval  11163  fac2  11294  faclbnd4lem1  11306  bcp1m1  11332  hashprg  11368  swrds2  11560  iseralt  12157  binom11  12290  climcndslem1  12308  climcndslem2  12309  ege2le3  12371  ef4p  12393  efgt1p2  12394  eirrlem  12482  odd2np1lem  12586  bitsfzolem  12625  bitsinv1lem  12632  isprm3  12767  prmind2  12769  opoe  12864  pockthlem  12952  pockthg  12953  prmunb  12961  prmreclem2  12964  4sqlem19  13010  vdwlem12  13039  decexp2  13090  2expltfac  13105  mulg2  14576  efgs1b  15045  efgredlemc  15054  lt6abl  15181  abvtrivd  15605  pjthlem1  18801  ovolunlem1a  18855  ovolicc1  18875  vitalilem2  18964  itgcnlem  19144  dveflem  19326  coskpi  19888  ang180lem3  20109  tanatan  20215  cosatan  20217  atantayl2  20234  emcllem7  20295  basellem3  20320  basellem5  20322  basellem8  20325  issqf  20374  ppi2  20408  ppi3  20409  cht2  20410  ppieq0  20414  ppiublem2  20442  chpeq0  20447  chtublem  20450  chtub  20451  chpub  20459  mersenne  20466  perfectlem2  20469  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  bposlem2  20524  bposlem6  20528  lgslem1  20535  lgsval2lem  20545  lgsdir2lem2  20563  lgsdir2lem3  20564  lgsdirprm  20568  lgseisen  20592  m1lgs  20601  rplogsumlem1  20633  rplogsumlem2  20634  dchrisum0flb  20659  dchrisum0re  20662  mulog2sumlem2  20684  pntrmax  20713  pntpbnd2  20736  pntibndlem2  20740  pntlemg  20747  pntlemr  20751  ex-fl  20834  1p1e2apr1  20839  vc2  21111  ipval2  21280  ip2i  21406  hv2times  21640  pjhthlem1  21970  ho2times  22399  stm1addi  22825  staddi  22826  stadd3i  22828  addltmulALT  23026  subfacp1lem1  23710  subfacp1lem5  23715  subfacp1lem6  23716  vdgr1d  23894  konigsberg  23911  axlowdimlem4  24573  axlowdimlem13  24582  bpoly1  24786  bpolydiflem  24789  bpoly3  24793  bpoly4  24794  intset  26044  pell14qrgapw  26961  rmydioph  27107  rmxdioph  27109  expdiophlem1  27114  expdiophlem2  27115  expdioph  27116  psgnunilem2  27418  stoweidlem14  27763  wallispilem3  27816  wallispi2lem2  27821
  Copyright terms: Public domain W3C validator