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

Definition df-2 10063
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 10054 . 2  class  2
2 c1 8996 . . 3  class  1
3 caddc 8998 . . 3  class  +
42, 2, 3co 6084 . 2  class  ( 1  +  1 )
51, 4wceq 1653 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  10074  2pos  10087  1p1e2  10099  2p2e4  10103  2times  10104  3p2e5  10116  4p2e6  10118  5p2e7  10121  6p2e8  10125  7p2e9  10128  8p2e10  10130  2nn  10138  1lt2  10147  nneo  10358  6p6e12  10438  7p5e12  10440  8p4e12  10444  9p2e11  10449  9p3e12  10450  eluz2b1  10552  x2times  10883  fztp  11107  fzprval  11111  fztpval  11112  fzo12sn  11188  sqval  11446  fac2  11577  faclbnd4lem1  11589  bcp1m1  11616  hashprg  11671  swrds2  11885  iseralt  12483  binom11  12616  climcndslem1  12634  climcndslem2  12635  ege2le3  12697  ef4p  12719  efgt1p2  12720  eirrlem  12808  odd2np1lem  12912  bitsfzolem  12951  isprm3  13093  prmind2  13095  opoe  13190  pockthlem  13278  pockthg  13279  prmunb  13287  prmreclem2  13290  4sqlem19  13336  vdwlem12  13365  decexp2  13416  2expltfac  13431  mulg2  14904  efgs1b  15373  efgredlemc  15382  lt6abl  15509  abvtrivd  15933  pjthlem1  19343  ovolunlem1a  19397  ovolicc1  19417  vitalilem2  19506  itgcnlem  19684  dveflem  19868  coskpi  20433  ang180lem3  20658  tanatan  20764  cosatan  20766  atantayl2  20783  emcllem7  20845  basellem3  20870  basellem5  20872  basellem8  20875  issqf  20924  ppi2  20958  ppi3  20959  cht2  20960  ppieq0  20964  ppiublem2  20992  chpeq0  20997  chtub  21001  chpub  21009  mersenne  21016  perfectlem2  21019  bcp1ctr  21068  bclbnd  21069  bposlem1  21073  bposlem2  21074  bposlem6  21078  lgslem1  21085  lgsval2lem  21095  lgsdir2lem2  21113  lgsdir2lem3  21114  lgsdirprm  21118  lgseisen  21142  m1lgs  21151  rplogsumlem1  21183  rplogsumlem2  21184  dchrisum0flb  21209  dchrisum0re  21212  mulog2sumlem2  21234  pntrmax  21263  pntpbnd2  21286  pntibndlem2  21290  pntlemg  21297  pntlemr  21301  constr3trllem3  21644  constr3pthlem1  21647  constr3pthlem3  21649  vdgr1d  21679  konigsberg  21714  ex-fl  21760  1p1e2apr1  21765  vc2  22039  ipval2  22208  ip2i  22334  hv2times  22568  pjhthlem1  22898  ho2times  23327  stm1addi  23753  staddi  23754  stadd3i  23756  addltmulALT  23954  subfacp1lem1  24870  subfacp1lem5  24875  subfacp1lem6  24876  axlowdimlem4  25889  axlowdimlem13  25898  bpoly1  26102  bpolydiflem  26105  bpoly3  26109  bpoly4  26110  sin2h  26250  tan2h  26252  itg2addnclem3  26271  pell14qrgapw  26952  rmydioph  27098  rmxdioph  27100  expdiophlem1  27105  expdiophlem2  27106  expdioph  27107  psgnunilem2  27408  stoweidlem14  27752  wallispilem3  27805  wallispi2lem2  27810  prmgt1  28256
  Copyright terms: Public domain W3C validator