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

Definition df-3 10957
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 10948 . 2 class 3
2 c2 10947 . . 3 class 2
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (2 + 1)
61, 5wceq 1475 1 wff 3 = (2 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  3re  10971  3pos  10991  3m1e2  11014  2p2e4  11021  2p1e3  11028  3p3e6  11038  4p3e7  11040  5p3e8  11043  6p3e9  11047  7p3e10OLD  11050  3t3e9  11057  3nn  11063  2lt3  11072  7p3e10  11479  7p6e13  11484  8p3e11  11488  8p3e11OLD  11489  8p5e13  11491  9p3e12  11497  9p4e13  11498  4t3e12  11508  5t3e15  11511  5t3e15OLD  11512  6t3e18  11518  7t3e21  11525  8t3e24  11531  9t3e27  11540  nn01to3  11657  fztpval  12272  fz0to3un2pr  12310  fz0to4untppr  12311  fzo0to42pr  12422  fzo1to4tp  12423  cu2  12825  i3  12828  binom3  12847  fac3  12929  hashtpg  13121  sqrlem7  13837  bpoly2  14627  bpoly4  14629  fsumcube  14630  ege2le3  14659  ef4p  14682  cos1bnd  14756  3prm  15244  oddprmge3  15250  prmgaplem3  15595  13prm  15661  23prm  15664  43prm  15667  83prm  15668  163prm  15670  lt6abl  18119  cphipval  22850  vitalilem4  23186  iblcnlem1  23360  itgcnlem  23362  dveflem  23546  sincosq3sgn  24056  sincosq4sgn  24057  tangtx  24061  sincos6thpi  24071  ang180lem2  24340  mcubic  24374  cubic2  24375  binom4  24377  dquartlem2  24379  quart1  24383  quartlem1  24384  log2ublem3  24475  basellem5  24611  basellem8  24614  basellem9  24615  ppi3  24697  cht3  24699  ppiublem1  24727  ppiublem2  24728  ppiub  24729  chtub  24737  bclbnd  24805  bposlem2  24810  bposlem9  24817  lgsdir2lem3  24852  dchrvmasumiflem1  24990  mulog2sumlem2  25024  pntlemk  25095  pntlemo  25096  axlowdimlem3  25624  axlowdimlem13  25634  axlowdimlem16  25637  axlowdimlem17  25638  constr3trllem3  26180  konigsberg  26514  extwwlkfablem2  26605  numclwwlkovf2ex  26613  ipval2  26946  stm1add3i  28490  stadd3i  28491  problem2  30813  problem2OLD  30814  problem4  30816  sinccvglem  30820  mblfinlem3  32618  heiborlem6  32785  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  amgm3d  37524  stoweidlem26  38919  31prm  40050  lighneallem4b  40064  3odd  40155  21wlkdlem1  41132  elwwlks2s3  41169  elwspths2spth  41171  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsberglem5  41426  av-numclwwlkovf2ex  41517
  Copyright terms: Public domain W3C validator