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

Definition df-3 10061
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 10052 . 2  class  3
2 c2 10051 . . 3  class  2
3 c1 8993 . . 3  class  1
4 caddc 8995 . . 3  class  +
52, 3, 4co 6083 . 2  class  ( 2  +  1 )
61, 5wceq 1653 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  10073  3pos  10086  3m1e2  10098  3m1e2OLD  10099  2p2e4  10100  2p1e3  10105  3p3e6  10114  4p3e7  10116  5p3e8  10119  6p3e9  10123  7p3e10  10126  3t3e9  10131  3nn  10136  2lt3  10145  7p6e13  10438  8p3e11  10440  8p5e13  10442  9p3e12  10447  9p4e13  10448  4t3e12  10456  5t3e15  10458  6t3e18  10462  7t3e21  10467  8t3e24  10473  9t3e27  10480  fztpval  11109  fzo0to42pr  11188  cu2  11481  i3  11484  binom3  11502  fac3  11575  hashtpg  11693  sqrlem7  12056  ege2le3  12694  ef4p  12716  cos1bnd  12790  3prm  13098  13prm  13440  23prm  13443  43prm  13446  83prm  13447  163prm  13449  lt6abl  15506  vitalilem4  19505  iblcnlem1  19681  itgcnlem  19683  dveflem  19865  sincosq3sgn  20410  sincosq4sgn  20411  tangtx  20415  sincos6thpi  20425  ang180lem2  20654  mcubic  20689  cubic2  20690  binom4  20692  dquartlem2  20694  quart1  20698  quartlem1  20699  log2ublem3  20790  basellem5  20869  basellem8  20872  basellem9  20873  ppi3  20956  cht3  20958  ppiublem1  20988  ppiublem2  20989  ppiub  20990  chtub  20998  bclbnd  21066  bposlem2  21071  bposlem9  21078  lgsdir2lem3  21111  dchrvmasumiflem1  21197  mulog2sumlem2  21231  pntlemk  21302  pntlemo  21303  usgraexvlem  21416  constr3trllem3  21641  konigsberg  21711  ipval2  22205  stm1add3i  23752  stadd3i  23753  sinccvglem  25111  axlowdimlem3  25885  axlowdimlem13  25895  axlowdimlem16  25898  axlowdimlem17  25899  bpoly2  26105  bpoly4  26107  fsumcube  26108  mblfinlem3  26247  heiborlem6  26527  rabren3dioph  26878  rmydioph  27087  rmxdioph  27089  expdiophlem2  27095  expdioph  27096  stoweidlem26  27753
  Copyright terms: Public domain W3C validator