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 10923
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 10914 . 2 class 3
2 c2 10913 . . 3 class 2
3 c1 9789 . . 3 class 1
4 caddc 9791 . . 3 class +
52, 3, 4co 6523 . 2 class (2 + 1)
61, 5wceq 1474 1 wff 3 = (2 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  3re  10937  3pos  10957  3m1e2  10980  2p2e4  10987  2p1e3  10994  3p3e6  11004  4p3e7  11006  5p3e8  11009  6p3e9  11013  7p3e10OLD  11016  3t3e9  11023  3nn  11029  2lt3  11038  7p3e10  11431  7p6e13  11436  8p3e11  11440  8p3e11OLD  11441  8p5e13  11443  9p3e12  11449  9p4e13  11450  4t3e12  11460  5t3e15  11463  5t3e15OLD  11464  6t3e18  11470  7t3e21  11477  8t3e24  11483  9t3e27  11492  nn01to3  11609  fztpval  12223  fz0to3un2pr  12261  fz0to4untppr  12262  fzo0to42pr  12373  fzo1to4tp  12374  cu2  12776  i3  12779  binom3  12798  fac3  12880  hashtpg  13067  sqrlem7  13779  bpoly2  14569  bpoly4  14571  fsumcube  14572  ege2le3  14601  ef4p  14624  cos1bnd  14698  3prm  15186  oddprmge3  15192  prmgaplem3  15537  13prm  15603  23prm  15606  43prm  15609  83prm  15610  163prm  15612  lt6abl  18061  vitalilem4  23099  iblcnlem1  23273  itgcnlem  23275  dveflem  23459  sincosq3sgn  23969  sincosq4sgn  23970  tangtx  23974  sincos6thpi  23984  ang180lem2  24253  mcubic  24287  cubic2  24288  binom4  24290  dquartlem2  24292  quart1  24296  quartlem1  24297  log2ublem3  24388  basellem5  24524  basellem8  24527  basellem9  24528  ppi3  24610  cht3  24612  ppiublem1  24640  ppiublem2  24641  ppiub  24642  chtub  24650  bclbnd  24718  bposlem2  24723  bposlem9  24730  lgsdir2lem3  24765  dchrvmasumiflem1  24903  mulog2sumlem2  24937  pntlemk  25008  pntlemo  25009  axlowdimlem3  25538  axlowdimlem13  25548  axlowdimlem16  25551  axlowdimlem17  25552  constr3trllem3  25942  konigsberg  26276  extwwlkfablem2  26367  numclwwlkovf2ex  26375  ipval2  26743  stm1add3i  28292  stadd3i  28293  problem2  30615  problem2OLD  30616  problem4  30618  sinccvglem  30622  mblfinlem3  32417  heiborlem6  32584  rmydioph  36398  rmxdioph  36400  expdiophlem2  36406  expdioph  36407  amgm3d  37323  stoweidlem26  38719  31prm  39851  lighneallem4b  39865  3odd  39956  21wlkdlem1  41130  elwwlks2s3  41167  elwspths2spth  41169  upgr3v3e3cycl  41345  upgr4cycl4dv4e  41350  konigsberglem5  41424  av-numclwwlkovf2ex  41515
  Copyright terms: Public domain W3C validator