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

Definition df-3 10015
Description: Define the number 3. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-3  |-  3  =  ( 2  +  1 )

Detailed syntax breakdown of Definition df-3
StepHypRef Expression
1 c3 10006 . 2  class  3
2 c2 10005 . . 3  class  2
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 2  +  1 )
61, 5wceq 1649 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  10027  3pos  10040  3m1e2  10052  3m1e2OLD  10053  2p2e4  10054  2p1e3  10059  3p3e6  10068  4p3e7  10070  5p3e8  10073  6p3e9  10077  7p3e10  10080  3t3e9  10085  3nn  10090  2lt3  10099  7p6e13  10392  8p3e11  10394  8p5e13  10396  9p3e12  10401  9p4e13  10402  4t3e12  10410  5t3e15  10412  6t3e18  10416  7t3e21  10421  8t3e24  10427  9t3e27  10434  fztpval  11063  fzo0to42pr  11141  cu2  11434  i3  11437  binom3  11455  fac3  11528  hashtpg  11646  sqrlem7  12009  ege2le3  12647  ef4p  12669  cos1bnd  12743  3prm  13051  13prm  13393  23prm  13396  43prm  13399  83prm  13400  163prm  13402  lt6abl  15459  vitalilem4  19456  iblcnlem1  19632  itgcnlem  19634  dveflem  19816  sincosq3sgn  20361  sincosq4sgn  20362  tangtx  20366  sincos6thpi  20376  ang180lem2  20605  mcubic  20640  cubic2  20641  binom4  20643  dquartlem2  20645  quart1  20649  quartlem1  20650  log2ublem3  20741  basellem5  20820  basellem8  20823  basellem9  20824  ppi3  20907  cht3  20909  ppiublem1  20939  ppiublem2  20940  ppiub  20941  chtub  20949  bclbnd  21017  bposlem2  21022  bposlem9  21029  lgsdir2lem3  21062  dchrvmasumiflem1  21148  mulog2sumlem2  21182  pntlemk  21253  pntlemo  21254  usgraexvlem  21367  constr3trllem3  21592  konigsberg  21662  ipval2  22156  stm1add3i  23703  stadd3i  23704  sinccvglem  25062  axlowdimlem3  25787  axlowdimlem13  25797  axlowdimlem16  25800  axlowdimlem17  25801  bpoly2  26007  bpoly4  26009  fsumcube  26010  mblfinlem2  26144  heiborlem6  26415  rabren3dioph  26766  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  stoweidlem26  27642
  Copyright terms: Public domain W3C validator