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

Definition df-2 9684
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 9675 . 2  class  2
2 c1 8618 . . 3  class  1
3 caddc 8620 . . 3  class  +
42, 2, 3co 5710 . 2  class  ( 1  +  1 )
51, 4wceq 1619 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9695  2pos  9708  1p1e2  9720  2p2e4  9721  2times  9722  3p2e5  9734  4p2e6  9736  5p2e7  9739  6p2e8  9743  7p2e9  9746  8p2e10  9748  2nn  9756  1lt2  9765  nneo  9974  6p6e12  10054  7p5e12  10056  8p4e12  10060  9p2e11  10065  9p3e12  10066  eluz2b1  10168  x2times  10497  fztp  10719  fzprval  10722  fztpval  10723  sqval  11041  fac2  11172  faclbnd4lem1  11184  bcp1m1  11210  hashprg  11245  swrds2  11437  iseralt  12034  binom11  12167  climcndslem1  12182  climcndslem2  12183  ege2le3  12245  ef4p  12267  efgt1p2  12268  eirrlem  12356  odd2np1lem  12460  bitsfzolem  12499  bitsinv1lem  12506  isprm3  12641  prmind2  12643  opoe  12738  pockthlem  12826  pockthg  12827  prmunb  12835  prmreclem2  12838  4sqlem19  12884  vdwlem12  12913  decexp2  12964  2expltfac  12979  mulg2  14411  efgs1b  14880  efgredlemc  14889  lt6abl  15016  abvtrivd  15440  pjthlem1  18633  ovolunlem1a  18687  ovolicc1  18707  vitalilem2  18796  itgcnlem  18976  dveflem  19158  coskpi  19720  ang180lem3  19941  tanatan  20047  cosatan  20049  atantayl2  20066  emcllem7  20127  basellem3  20152  basellem5  20154  basellem8  20157  issqf  20206  ppi2  20240  ppi3  20241  cht2  20242  ppieq0  20246  ppiublem2  20274  chpeq0  20279  chtublem  20282  chtub  20283  chpub  20291  mersenne  20298  perfectlem2  20301  bcp1ctr  20350  bclbnd  20351  bposlem1  20355  bposlem2  20356  bposlem6  20360  lgslem1  20367  lgsval2lem  20377  lgsdir2lem2  20395  lgsdir2lem3  20396  lgsdirprm  20400  lgseisen  20424  m1lgs  20433  rplogsumlem1  20465  rplogsumlem2  20466  dchrisum0flb  20491  dchrisum0re  20494  mulog2sumlem2  20516  pntrmax  20545  pntpbnd2  20568  pntibndlem2  20572  pntlemg  20579  pntlemr  20583  ex-fl  20647  1p1e2apr1  20669  vc2  20941  ipval2  21110  ip2i  21236  hv2times  21470  pjhthlem1  21800  ho2times  22229  stm1addi  22655  staddi  22656  stadd3i  22658  addltmulALT  22856  subfacp1lem1  22881  subfacp1lem5  22886  subfacp1lem6  22887  vdgr1d  23065  konigsberg  23082  axlowdimlem4  23747  axlowdimlem13  23756  bpoly1  23960  bpolydiflem  23963  bpoly3  23967  bpoly4  23968  intset  25210  pell14qrgapw  26127  rmydioph  26273  rmxdioph  26275  expdiophlem1  26280  expdiophlem2  26281  expdioph  26282  psgnunilem2  26584  stoweidlem14  26897
  Copyright terms: Public domain W3C validator