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 11680
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 11672 . 2 class 3
2 c2 11671 . . 3 class 2
3 c1 10516 . . 3 class 1
4 caddc 10518 . . 3 class +
52, 3, 4co 7133 . 2 class (2 + 1)
61, 5wceq 1537 1 wff 3 = (2 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  3nn  11695  3re  11696  3cn  11697  3pos  11721  3m1e2  11744  2p2e4  11751  2p1e3  11758  3p3e6  11768  4p3e7  11770  5p3e8  11773  6p3e9  11776  3t3e9  11783  2lt3  11788  7p3e10  12152  7p6e13  12155  8p3e11  12158  8p5e13  12160  9p3e12  12165  9p4e13  12166  4t3e12  12175  5t3e15  12178  6t3e18  12182  7t3e21  12187  8t3e24  12193  9t3e27  12200  nn01to3  12320  fztpval  12953  fz0to3un2pr  12993  fz0to4untppr  12994  fzo0to42pr  13108  fzo1to4tp  13109  cu2  13548  i3  13551  binom3  13570  fac3  13625  hashtpg  13828  sqrlem7  14588  bpoly2  15391  bpoly4  15393  fsumcube  15394  ege2le3  15423  ef4p  15446  cos1bnd  15520  oddprmge3  16022  prmgaplem3  16367  13prm  16428  23prm  16431  43prm  16434  83prm  16435  163prm  16437  lt6abl  18994  cphipval  23826  vitalilem4  24194  itgcnlem  24372  dveflem  24561  sincosq3sgn  25072  sincosq4sgn  25073  tangtx  25077  sincos6thpi  25087  ang180lem2  25375  mcubic  25412  cubic2  25413  binom4  25415  dquartlem2  25417  quart1  25421  quartlem1  25422  log2ublem3  25513  basellem5  25649  basellem8  25652  basellem9  25653  ppi3  25735  cht3  25737  ppiublem1  25765  ppiublem2  25766  ppiub  25767  chtub  25775  bclbnd  25843  bposlem2  25848  bposlem9  25855  lgsdir2lem3  25890  dchrvmasumiflem1  26064  mulog2sumlem2  26098  pntlemk  26169  pntlemo  26170  axlowdimlem3  26717  axlowdimlem13  26727  axlowdimlem16  26730  axlowdimlem17  26731  2wlkdlem1  27690  elwwlks2s3  27716  elwspths2spth  27732  upgr3v3e3cycl  27944  upgr4cycl4dv4e  27949  konigsberglem5  28020  ipval2  28469  stm1add3i  30009  stadd3i  30010  problem2  32917  problem4  32919  sinccvglem  32923  mblfinlem3  34972  heiborlem6  35130  fac2xp3  39206  sn-0ne2  39356  3cubeslem2  39419  3cubeslem3r  39421  rmydioph  39748  rmxdioph  39750  expdiophlem2  39756  expdioph  39757  amgm3d  40687  stoweidlem26  42459  31prm  43906  lighneallem4b  43919  3odd  44018  sbgoldbo  44097  itcoval3  44839  ackval3  44857
  Copyright terms: Public domain W3C validator