Definition df-3 12310

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

Step	Hyp	Ref	Expression
1		c3 12302	. 2 class 3
2		c2 12301	. . 3 class 2
3		c1 11107	. . 3 class 1
4		caddc 11109	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (2 + 1)
6	1, 5	wceq 1569	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12326  3re  12327  3cn  12328  3m1e2  12374  2p2e4  12381  2p1e3  12388  3p3e6  12398  4p3e7  12400  5p3e8  12403  6p3e9  12406  3t3e9  12414  2lt3  12420  7p3e10  12797  7p6e13  12800  8p3e11  12803  8p5e13  12805  9p3e12  12810  9p4e13  12811  4t3e12  12820  5t3e15  12823  6t3e18  12827  7t3e21  12832  8t3e24  12838  9t3e27  12845  nn01to3  12971  fztpval  13621  fz0to3un2pr  13664  fzo0to42pr  13789  fzo1to4tp  13790  cu2  14243  i3  14246  binom3  14267  fac3  14323  hashtpg  14529  01sqrexlem7  15306  bpoly2  16117  bpoly4  16119  fsumcube  16120  ege2le3  16150  ef4p  16175  cos1bnd  16249  oddprmge3  16765  prmgaplem3  17119  13prm  17182  23prm  17185  43prm  17188  83prm  17189  163prm  17191  lt6abl  19971  cphipval  25413  vitalilem4  25781  itgcnlem  25960  dveflem  26149  sincosq3sgn  26676  sincosq4sgn  26677  tangtx  26681  sincos6thpi  26692  ang180lem2  26986  mcubic  27023  cubic2  27024  binom4  27026  dquartlem2  27028  quart1  27032  quartlem1  27033  log2ublem3  27124  basellem5  27260  basellem9  27264  ppi3  27346  cht3  27348  ppiublem1  27377  ppiublem2  27378  ppiub  27379  chtub  27387  bclbnd  27455  bposlem2  27460  bposlem9  27467  lgsdir2lem3  27502  dchrvmasumiflem1  27676  mulog2sumlem2  27710  pntlemk  27781  pntlemo  27782  axlowdimlem3  29305  axlowdimlem13  29315  axlowdimlem16  29318  axlowdimlem17  29319  2wlkdlem1  30285  elwwlks2s3  30311  elwspths2spth  30330  upgr3v3e3cycl  30542  upgr4cycl4dv4e  30547  konigsberglem5  30618  ipval2  31070  stm1add3i  32610  stadd3i  32611  problem2  36166  problem4  36168  sinccvglem  36172  mblfinlem3  38338  heiborlem6  38495  aks4d1p1  42871  2ap1caineq  42940  1p3e4  43054  nicomachus  43101  sn-0ne2  43195  3cubeslem2  43444  3cubeslem3r  43446  rmydioph  43769  rmxdioph  43771  expdiophlem2  43777  expdioph  43778  amgm3d  44953  stoweidlem26  46768  sin3t  47636  cos3t  47637  sin5tlem1  47638  2timesltsq  48143  2timesltsqm1  48144  31prm  48377  lighneallem4b  48389  nprmdvdsfacm1lem2  48401  3odd  48501  sbgoldbo  48580  itcoval3  49473  ackval3  49491