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

Definition df-3 9805
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 9796 . 2  class  3
2 c2 9795 . . 3  class  2
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 2  +  1 )
61, 5wceq 1623 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  9817  3pos  9830  2p2e4  9842  2p1e3  9847  3p3e6  9856  4p3e7  9858  5p3e8  9861  6p3e9  9865  7p3e10  9868  3t3e9  9873  3nn  9878  2lt3  9887  halfpm6th  9936  7p6e13  10178  8p3e11  10180  8p5e13  10182  9p3e12  10187  9p4e13  10188  4t3e12  10196  5t3e15  10198  6t3e18  10202  7t3e21  10207  8t3e24  10213  9t3e27  10220  fztpval  10845  cu2  11201  i3  11204  binom3  11222  fac3  11295  sqrlem7  11734  ege2le3  12371  ef4p  12393  cos1bnd  12467  rpnnen2lem3  12495  rpnnen2lem11  12503  3prm  12775  13prm  13117  23prm  13120  43prm  13123  83prm  13124  163prm  13126  lt6abl  15181  vitalilem4  18966  iblcnlem1  19142  itgcnlem  19144  dveflem  19326  sincosq3sgn  19868  sincosq4sgn  19869  tangtx  19873  sincos6thpi  19883  ang180lem2  20108  mcubic  20143  cubic2  20144  binom4  20146  dquartlem2  20148  quart1  20152  quartlem1  20153  log2cnv  20240  log2ublem3  20244  basellem5  20322  basellem8  20325  basellem9  20326  ppi3  20409  cht3  20411  ppiublem1  20441  ppiublem2  20442  ppiub  20443  chtub  20451  bclbnd  20519  bposlem2  20524  bposlem9  20531  lgsdir2lem3  20564  dchrvmasumiflem1  20650  mulog2sumlem2  20684  pntlemk  20755  pntlemo  20756  ipval2  21280  stm1add3i  22827  stadd3i  22828  konigsberg  23911  sinccvglem  24005  axlowdimlem3  24572  axlowdimlem13  24582  axlowdimlem16  24585  axlowdimlem17  24586  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  3timesi  25178  2eq3m1  25179  heiborlem6  26540  rabren3dioph  26898  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  expdioph  27116  stoweidlem26  27775  usgraexvlem  28127
  Copyright terms: Public domain W3C validator