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

Definition df-3 9801
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 9792 . 2  class  3
2 c2 9791 . . 3  class  2
3 c1 8734 . . 3  class  1
4 caddc 8736 . . 3  class  +
52, 3, 4co 5820 . 2  class  ( 2  +  1 )
61, 5wceq 1624 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  9813  3pos  9826  2p2e4  9838  2p1e3  9843  3p3e6  9852  4p3e7  9854  5p3e8  9857  6p3e9  9861  7p3e10  9864  3t3e9  9869  3nn  9874  2lt3  9883  halfpm6th  9932  7p6e13  10174  8p3e11  10176  8p5e13  10178  9p3e12  10183  9p4e13  10184  4t3e12  10192  5t3e15  10194  6t3e18  10198  7t3e21  10203  8t3e24  10209  9t3e27  10216  fztpval  10840  cu2  11196  i3  11199  binom3  11217  fac3  11290  sqrlem7  11729  ege2le3  12366  ef4p  12388  cos1bnd  12462  rpnnen2lem3  12490  rpnnen2lem11  12498  3prm  12770  13prm  13112  23prm  13115  43prm  13118  83prm  13119  163prm  13121  lt6abl  15176  vitalilem4  18961  iblcnlem1  19137  itgcnlem  19139  dveflem  19321  sincosq3sgn  19863  sincosq4sgn  19864  tangtx  19868  sincos6thpi  19878  ang180lem2  20103  mcubic  20138  cubic2  20139  binom4  20141  dquartlem2  20143  quart1  20147  quartlem1  20148  log2cnv  20235  log2ublem3  20239  basellem5  20317  basellem8  20320  basellem9  20321  ppi3  20404  cht3  20406  ppiublem1  20436  ppiublem2  20437  ppiub  20438  chtub  20446  bclbnd  20514  bposlem2  20519  bposlem9  20526  lgsdir2lem3  20559  dchrvmasumiflem1  20645  mulog2sumlem2  20679  pntlemk  20750  pntlemo  20751  ipval2  21273  stm1add3i  22820  stadd3i  22821  konigsberg  23316  sinccvglem  23410  axlowdimlem3  23980  axlowdimlem13  23990  axlowdimlem16  23993  axlowdimlem17  23994  bpoly2  24200  bpoly3  24201  bpoly4  24202  fsumcube  24203  3timesi  24578  2eq3m1  24579  heiborlem6  25940  rabren3dioph  26298  rmydioph  26507  rmxdioph  26509  expdiophlem2  26515  expdioph  26516  stoweidlem26  27175
  Copyright terms: Public domain W3C validator