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

Definition df-2 9799
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 9790 . 2  class  2
2 c1 8733 . . 3  class  1
3 caddc 8735 . . 3  class  +
42, 2, 3co 5819 . 2  class  ( 1  +  1 )
51, 4wceq 1624 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9810  2pos  9823  1p1e2  9835  2p2e4  9837  2times  9838  3p2e5  9850  4p2e6  9852  5p2e7  9855  6p2e8  9859  7p2e9  9862  8p2e10  9864  2nn  9872  1lt2  9881  nneo  10090  6p6e12  10170  7p5e12  10172  8p4e12  10176  9p2e11  10181  9p3e12  10182  eluz2b1  10284  x2times  10613  fztp  10835  fzprval  10838  fztpval  10839  sqval  11157  fac2  11288  faclbnd4lem1  11300  bcp1m1  11326  hashprg  11362  swrds2  11554  iseralt  12151  binom11  12284  climcndslem1  12302  climcndslem2  12303  ege2le3  12365  ef4p  12387  efgt1p2  12388  eirrlem  12476  odd2np1lem  12580  bitsfzolem  12619  bitsinv1lem  12626  isprm3  12761  prmind2  12763  opoe  12858  pockthlem  12946  pockthg  12947  prmunb  12955  prmreclem2  12958  4sqlem19  13004  vdwlem12  13033  decexp2  13084  2expltfac  13099  mulg2  14570  efgs1b  15039  efgredlemc  15048  lt6abl  15175  abvtrivd  15599  pjthlem1  18795  ovolunlem1a  18849  ovolicc1  18869  vitalilem2  18958  itgcnlem  19138  dveflem  19320  coskpi  19882  ang180lem3  20103  tanatan  20209  cosatan  20211  atantayl2  20228  emcllem7  20289  basellem3  20314  basellem5  20316  basellem8  20319  issqf  20368  ppi2  20402  ppi3  20403  cht2  20404  ppieq0  20408  ppiublem2  20436  chpeq0  20441  chtublem  20444  chtub  20445  chpub  20453  mersenne  20460  perfectlem2  20463  bcp1ctr  20512  bclbnd  20513  bposlem1  20517  bposlem2  20518  bposlem6  20522  lgslem1  20529  lgsval2lem  20539  lgsdir2lem2  20557  lgsdir2lem3  20558  lgsdirprm  20562  lgseisen  20586  m1lgs  20595  rplogsumlem1  20627  rplogsumlem2  20628  dchrisum0flb  20653  dchrisum0re  20656  mulog2sumlem2  20678  pntrmax  20707  pntpbnd2  20730  pntibndlem2  20734  pntlemg  20741  pntlemr  20745  ex-fl  20809  1p1e2apr1  20831  vc2  21103  ipval2  21272  ip2i  21398  hv2times  21632  pjhthlem1  21962  ho2times  22391  stm1addi  22817  staddi  22818  stadd3i  22820  addltmulALT  23018  subfacp1lem1  23114  subfacp1lem5  23119  subfacp1lem6  23120  vdgr1d  23298  konigsberg  23315  axlowdimlem4  23980  axlowdimlem13  23989  bpoly1  24193  bpolydiflem  24196  bpoly3  24200  bpoly4  24201  intset  25443  pell14qrgapw  26360  rmydioph  26506  rmxdioph  26508  expdiophlem1  26513  expdiophlem2  26514  expdioph  26515  psgnunilem2  26817  stoweidlem14  27162  wallispilem3  27215  wallispi2lem2  27220
  Copyright terms: Public domain W3C validator