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

Definition df-2 9758
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 9749 . 2  class  2
2 c1 8692 . . 3  class  1
3 caddc 8694 . . 3  class  +
42, 2, 3co 5778 . 2  class  ( 1  +  1 )
51, 4wceq 1619 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9769  2pos  9782  1p1e2  9794  2p2e4  9795  2times  9796  3p2e5  9808  4p2e6  9810  5p2e7  9813  6p2e8  9817  7p2e9  9820  8p2e10  9822  2nn  9830  1lt2  9839  nneo  10048  6p6e12  10128  7p5e12  10130  8p4e12  10134  9p2e11  10139  9p3e12  10140  eluz2b1  10242  x2times  10571  fztp  10793  fzprval  10796  fztpval  10797  sqval  11115  fac2  11246  faclbnd4lem1  11258  bcp1m1  11284  hashprg  11319  swrds2  11511  iseralt  12108  binom11  12241  climcndslem1  12256  climcndslem2  12257  ege2le3  12319  ef4p  12341  efgt1p2  12342  eirrlem  12430  odd2np1lem  12534  bitsfzolem  12573  bitsinv1lem  12580  isprm3  12715  prmind2  12717  opoe  12812  pockthlem  12900  pockthg  12901  prmunb  12909  prmreclem2  12912  4sqlem19  12958  vdwlem12  12987  decexp2  13038  2expltfac  13053  mulg2  14524  efgs1b  14993  efgredlemc  15002  lt6abl  15129  abvtrivd  15553  pjthlem1  18749  ovolunlem1a  18803  ovolicc1  18823  vitalilem2  18912  itgcnlem  19092  dveflem  19274  coskpi  19836  ang180lem3  20057  tanatan  20163  cosatan  20165  atantayl2  20182  emcllem7  20243  basellem3  20268  basellem5  20270  basellem8  20273  issqf  20322  ppi2  20356  ppi3  20357  cht2  20358  ppieq0  20362  ppiublem2  20390  chpeq0  20395  chtublem  20398  chtub  20399  chpub  20407  mersenne  20414  perfectlem2  20417  bcp1ctr  20466  bclbnd  20467  bposlem1  20471  bposlem2  20472  bposlem6  20476  lgslem1  20483  lgsval2lem  20493  lgsdir2lem2  20511  lgsdir2lem3  20512  lgsdirprm  20516  lgseisen  20540  m1lgs  20549  rplogsumlem1  20581  rplogsumlem2  20582  dchrisum0flb  20607  dchrisum0re  20610  mulog2sumlem2  20632  pntrmax  20661  pntpbnd2  20684  pntibndlem2  20688  pntlemg  20695  pntlemr  20699  ex-fl  20763  1p1e2apr1  20785  vc2  21057  ipval2  21226  ip2i  21352  hv2times  21586  pjhthlem1  21916  ho2times  22345  stm1addi  22771  staddi  22772  stadd3i  22774  addltmulALT  22972  subfacp1lem1  23068  subfacp1lem5  23073  subfacp1lem6  23074  vdgr1d  23252  konigsberg  23269  axlowdimlem4  23934  axlowdimlem13  23943  bpoly1  24147  bpolydiflem  24150  bpoly3  24154  bpoly4  24155  intset  25397  pell14qrgapw  26314  rmydioph  26460  rmxdioph  26462  expdiophlem1  26467  expdiophlem2  26468  expdioph  26469  psgnunilem2  26771  stoweidlem14  27084
  Copyright terms: Public domain W3C validator