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

Definition df-3 9850
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 9841 . 2  class  3
2 c2 9840 . . 3  class  2
3 c1 8783 . . 3  class  1
4 caddc 8785 . . 3  class  +
52, 3, 4co 5900 . 2  class  ( 2  +  1 )
61, 5wceq 1633 1  wff  3  =  ( 2  +  1 )
Colors of variables: wff set class
This definition is referenced by:  3re  9862  3pos  9875  3m1e2  9887  3m1e2OLD  9888  2p2e4  9889  2p1e3  9894  3p3e6  9903  4p3e7  9905  5p3e8  9908  6p3e9  9912  7p3e10  9915  3t3e9  9920  3nn  9925  2lt3  9934  halfpm6th  9983  7p6e13  10225  8p3e11  10227  8p5e13  10229  9p3e12  10234  9p4e13  10235  4t3e12  10243  5t3e15  10245  6t3e18  10249  7t3e21  10254  8t3e24  10260  9t3e27  10267  fztpval  10892  cu2  11248  i3  11251  binom3  11269  fac3  11342  sqrlem7  11781  ege2le3  12418  ef4p  12440  cos1bnd  12514  rpnnen2lem3  12542  rpnnen2lem11  12550  3prm  12822  13prm  13164  23prm  13167  43prm  13170  83prm  13171  163prm  13173  lt6abl  15230  vitalilem4  19019  iblcnlem1  19195  itgcnlem  19197  dveflem  19379  sincosq3sgn  19921  sincosq4sgn  19922  tangtx  19926  sincos6thpi  19936  ang180lem2  20161  mcubic  20196  cubic2  20197  binom4  20199  dquartlem2  20201  quart1  20205  quartlem1  20206  log2cnv  20293  log2ublem3  20297  basellem5  20375  basellem8  20378  basellem9  20379  ppi3  20462  cht3  20464  ppiublem1  20494  ppiublem2  20495  ppiub  20496  chtub  20504  bclbnd  20572  bposlem2  20577  bposlem9  20584  lgsdir2lem3  20617  dchrvmasumiflem1  20703  mulog2sumlem2  20737  pntlemk  20808  pntlemo  20809  ipval2  21335  stm1add3i  22882  stadd3i  22883  konigsberg  24195  sinccvglem  24289  axlowdimlem3  24958  axlowdimlem13  24968  axlowdimlem16  24971  axlowdimlem17  24972  bpoly2  25178  bpoly3  25179  bpoly4  25180  fsumcube  25181  heiborlem6  25688  rabren3dioph  26046  rmydioph  26255  rmxdioph  26257  expdiophlem2  26263  expdioph  26264  stoweidlem26  26923  fzo0to3tp  27272  fzo0to42pr  27273  hashtpg  27279  usgraexvlem  27360  constr3trllem3  27536
  Copyright terms: Public domain W3C validator