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 11077
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 11068 . 2 class 3
2 c2 11067 . . 3 class 2
3 c1 9934 . . 3 class 1
4 caddc 9936 . . 3 class +
52, 3, 4co 6647 . 2 class (2 + 1)
61, 5wceq 1482 1 wff 3 = (2 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  3re  11091  3pos  11111  3m1e2  11134  2p2e4  11141  2p1e3  11148  3p3e6  11158  4p3e7  11160  5p3e8  11163  6p3e9  11167  7p3e10OLD  11170  3t3e9  11177  3nn  11183  2lt3  11192  7p3e10  11600  7p6e13  11605  8p3e11  11609  8p3e11OLD  11610  8p5e13  11612  9p3e12  11618  9p4e13  11619  4t3e12  11629  5t3e15  11632  5t3e15OLD  11633  6t3e18  11639  7t3e21  11646  8t3e24  11652  9t3e27  11661  nn01to3  11778  fztpval  12399  fz0to3un2pr  12437  fz0to4untppr  12438  fzo0to42pr  12551  fzo1to4tp  12552  cu2  12958  i3  12961  binom3  12980  fac3  13062  hashtpg  13262  sqrlem7  13983  bpoly2  14782  bpoly4  14784  fsumcube  14785  ege2le3  14814  ef4p  14837  cos1bnd  14911  3prm  15400  oddprmge3  15406  prmgaplem3  15751  13prm  15817  23prm  15820  43prm  15823  83prm  15824  163prm  15826  lt6abl  18290  cphipval  23036  vitalilem4  23374  iblcnlem1  23548  itgcnlem  23550  dveflem  23736  sincosq3sgn  24246  sincosq4sgn  24247  tangtx  24251  sincos6thpi  24261  ang180lem2  24534  mcubic  24568  cubic2  24569  binom4  24571  dquartlem2  24573  quart1  24577  quartlem1  24578  log2ublem3  24669  basellem5  24805  basellem8  24808  basellem9  24809  ppi3  24891  cht3  24893  ppiublem1  24921  ppiublem2  24922  ppiub  24923  chtub  24931  bclbnd  24999  bposlem2  25004  bposlem9  25011  lgsdir2lem3  25046  dchrvmasumiflem1  25184  mulog2sumlem2  25218  pntlemk  25289  pntlemo  25290  axlowdimlem3  25818  axlowdimlem13  25828  axlowdimlem16  25831  axlowdimlem17  25832  2wlkdlem1  26815  elwwlks2s3  26853  elwspths2spth  26856  upgr3v3e3cycl  27033  upgr4cycl4dv4e  27038  konigsberglem5  27111  numclwwlkovf2ex  27204  ipval2  27546  stm1add3i  29090  stadd3i  29091  problem2  31544  problem2OLD  31545  problem4  31547  sinccvglem  31551  mblfinlem3  33428  heiborlem6  33595  rmydioph  37407  rmxdioph  37409  expdiophlem2  37415  expdioph  37416  amgm3d  38328  stoweidlem26  40012  31prm  41283  lighneallem4b  41297  3odd  41388  sbgoldbo  41446
  Copyright terms: Public domain W3C validator