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

Definition df-2 9652
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 9643 . 2  class  2
2 c1 8615 . . 3  class  1
3 caddc 8617 . . 3  class  +
42, 2, 3co 5707 . 2  class  ( 1  +  1 )
51, 4wceq 1619 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9663  2pos  9676  1p1e2  9688  2p2e4  9689  2times  9690  3p2e5  9702  4p2e6  9704  5p2e7  9707  6p2e8  9711  7p2e9  9714  8p2e10  9716  2nn  9724  1lt2  9733  nneo  9941  6p6e12  10021  7p5e12  10023  8p4e12  10027  9p2e11  10032  9p3e12  10033  eluz2b1  10135  x2times  10464  fztp  10684  fzprval  10687  fztpval  10688  sqval  11006  fac2  11136  faclbnd4lem1  11148  bcp1m1  11174  hashprg  11209  swrds2  11401  iseralt  11996  binom11  12129  climcndslem1  12144  climcndslem2  12145  ege2le3  12207  ef4p  12229  efgt1p2  12230  eirrlem  12318  odd2np1lem  12422  bitsfzolem  12461  bitsinv1lem  12468  isprm3  12603  prmind2  12605  opoe  12700  pockthlem  12788  pockthg  12789  prmunb  12797  prmreclem2  12800  4sqlem19  12846  vdwlem12  12875  decexp2  12926  2expltfac  12941  mulg2  14373  efgs1b  14842  efgredlemc  14851  lt6abl  14978  abvtrivd  15402  pjthlem1  18595  ovolunlem1a  18649  ovolicc1  18669  vitalilem2  18758  itgcnlem  18938  dveflem  19120  coskpi  19678  ang180lem3  19800  tanatan  19981  cosatan  19983  atantayl2  20000  emcllem7  20061  basellem3  20086  basellem5  20088  basellem8  20091  issqf  20140  ppi2  20174  ppi3  20175  cht2  20176  ppieq0  20180  ppiublem2  20208  chpeq0  20213  chtublem  20216  chtub  20217  chpub  20225  mersenne  20232  perfectlem2  20235  bcp1ctr  20284  bclbnd  20285  bposlem1  20289  bposlem2  20290  bposlem6  20294  lgslem1  20301  lgsval2lem  20311  lgsdir2lem2  20329  lgsdir2lem3  20330  lgsdirprm  20334  lgseisen  20358  m1lgs  20367  rplogsumlem1  20399  rplogsumlem2  20400  dchrisum0flb  20425  dchrisum0re  20428  mulog2sumlem2  20450  pntrmax  20479  pntpbnd2  20502  pntibndlem2  20506  pntlemg  20513  pntlemr  20517  ex-fl  20581  1p1e2apr1  20600  vc2  20872  ipval2  21041  ip2i  21167  hv2times  21401  pjhthlem1  21731  ho2times  22160  stm1addi  22586  staddi  22587  stadd3i  22589  addltmulALT  22787  subfacp1lem1  22812  subfacp1lem5  22817  subfacp1lem6  22818  vdgr1d  22996  konigsberg  23013  axlowdimlem4  23678  axlowdimlem13  23687  bpoly1  23891  bpolydiflem  23894  bpoly3  23898  bpoly4  23899  intset  25141  pell14qrgapw  26058  rmydioph  26204  rmxdioph  26206  expdiophlem1  26211  expdiophlem2  26212  expdioph  26213  psgnunilem2  26515
  Copyright terms: Public domain W3C validator