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

Definition df-2 9820
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 9811 . 2  class  2
2 c1 8754 . . 3  class  1
3 caddc 8756 . . 3  class  +
42, 2, 3co 5874 . 2  class  ( 1  +  1 )
51, 4wceq 1632 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9831  2pos  9844  1p1e2  9856  2p2e4  9858  2times  9859  3p2e5  9871  4p2e6  9873  5p2e7  9876  6p2e8  9880  7p2e9  9883  8p2e10  9885  2nn  9893  1lt2  9902  nneo  10111  6p6e12  10191  7p5e12  10193  8p4e12  10197  9p2e11  10202  9p3e12  10203  eluz2b1  10305  x2times  10635  fztp  10857  fzprval  10860  fztpval  10861  sqval  11179  fac2  11310  faclbnd4lem1  11322  bcp1m1  11348  hashprg  11384  swrds2  11576  iseralt  12173  binom11  12306  climcndslem1  12324  climcndslem2  12325  ege2le3  12387  ef4p  12409  efgt1p2  12410  eirrlem  12498  odd2np1lem  12602  bitsfzolem  12641  bitsinv1lem  12648  isprm3  12783  prmind2  12785  opoe  12880  pockthlem  12968  pockthg  12969  prmunb  12977  prmreclem2  12980  4sqlem19  13026  vdwlem12  13055  decexp2  13106  2expltfac  13121  mulg2  14592  efgs1b  15061  efgredlemc  15070  lt6abl  15197  abvtrivd  15621  pjthlem1  18817  ovolunlem1a  18871  ovolicc1  18891  vitalilem2  18980  itgcnlem  19160  dveflem  19342  coskpi  19904  ang180lem3  20125  tanatan  20231  cosatan  20233  atantayl2  20250  emcllem7  20311  basellem3  20336  basellem5  20338  basellem8  20341  issqf  20390  ppi2  20424  ppi3  20425  cht2  20426  ppieq0  20430  ppiublem2  20458  chpeq0  20463  chtublem  20466  chtub  20467  chpub  20475  mersenne  20482  perfectlem2  20485  bcp1ctr  20534  bclbnd  20535  bposlem1  20539  bposlem2  20540  bposlem6  20544  lgslem1  20551  lgsval2lem  20561  lgsdir2lem2  20579  lgsdir2lem3  20580  lgsdirprm  20584  lgseisen  20608  m1lgs  20617  rplogsumlem1  20649  rplogsumlem2  20650  dchrisum0flb  20675  dchrisum0re  20678  mulog2sumlem2  20700  pntrmax  20729  pntpbnd2  20752  pntibndlem2  20756  pntlemg  20763  pntlemr  20767  ex-fl  20850  1p1e2apr1  20855  vc2  21127  ipval2  21296  ip2i  21422  hv2times  21656  pjhthlem1  21986  ho2times  22415  stm1addi  22841  staddi  22842  stadd3i  22844  addltmulALT  23042  subfacp1lem1  23725  subfacp1lem5  23730  subfacp1lem6  23731  vdgr1d  23909  konigsberg  23926  axlowdimlem4  24645  axlowdimlem13  24654  bpoly1  24858  bpolydiflem  24861  bpoly3  24865  bpoly4  24866  itg2addnc  25005  intset  26147  pell14qrgapw  27064  rmydioph  27210  rmxdioph  27212  expdiophlem1  27217  expdiophlem2  27218  expdioph  27219  psgnunilem2  27521  stoweidlem14  27866  wallispilem3  27919  wallispi2lem2  27924  constr3trllem3  28398  constr3pthlem1  28401  constr3pthlem3  28403
  Copyright terms: Public domain W3C validator