Definition df-3 12332

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 12324	. 2 class 3
2		c2 12323	. . 3 class 2
3		c1 11129	. . 3 class 1
4		caddc 11131	. . 3 class +
5	2, 3, 4	co 7417	. 2 class (2 + 1)
6	1, 5	wceq 1570	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12348  3re  12349  3cn  12350  3m1e2  12396  2p2e4  12403  2p1e3  12410  3p3e6  12420  4p3e7  12422  5p3e8  12425  6p3e9  12428  3t3e9  12436  2lt3  12442  7p3e10  12820  7p6e13  12823  8p3e11  12826  8p5e13  12828  9p3e12  12833  9p4e13  12834  4t3e12  12843  5t3e15  12846  6t3e18  12850  7t3e21  12855  8t3e24  12861  9t3e27  12868  nn01to3  12994  fztpval  13645  fz0to3un2pr  13688  fzo0to42pr  13813  fzo1to4tp  13814  cu2  14268  i3  14271  binom3  14292  fac3  14348  hashtpg  14554  01sqrexlem7  15339  bpoly2  16149  bpoly4  16151  fsumcube  16152  ege2le3  16182  ef4p  16207  cos1bnd  16281  oddprmge3  16797  prmgaplem3  17151  13prm  17214  23prm  17217  43prm  17220  83prm  17221  163prm  17223  lt6abl  20028  cphipval  25477  vitalilem4  25845  itgcnlem  26024  dveflem  26213  sincosq3sgn  26745  sincosq4sgn  26746  tangtx  26750  sincos6thpi  26761  ang180lem2  27055  mcubic  27092  cubic2  27093  binom4  27095  dquartlem2  27097  quart1  27101  quartlem1  27102  log2ublem3  27193  basellem5  27329  basellem9  27333  ppi3  27415  cht3  27417  ppiublem1  27446  ppiublem2  27447  ppiub  27448  chtub  27456  bclbnd  27524  bposlem2  27529  bposlem9  27536  lgsdir2lem3  27571  dchrvmasumiflem1  27745  mulog2sumlem2  27779  pntlemk  27850  pntlemo  27851  axlowdimlem3  29409  axlowdimlem13  29419  axlowdimlem16  29422  axlowdimlem17  29423  2wlkdlem1  30401  elwwlks2s3  30427  elwspths2spth  30446  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  konigsberglem5  30744  ipval2  31196  stm1add3i  32736  stadd3i  32737  problem2  36253  problem4  36255  sinccvglem  36259  mblfinlem3  38416  heiborlem6  38574  aks4d1p1  42950  2ap1caineq  43019  1p3e4  43134  nicomachus  43195  sn-0ne2  43289  3cubeslem2  43538  3cubeslem3r  43540  rmydioph  43863  rmxdioph  43865  expdiophlem2  43871  expdioph  43872  amgm3d  45047  stoweidlem26  46862  sin3t  47743  cos3t  47744  sin5tlem1  47745  goldpolyfactor  47753  2timesltsq  48274  2timesltsqm1  48275  31prm  48508  lighneallem4b  48520  nprmdvdsfacm1lem2  48532  3odd  48632  sbgoldbo  48711  itcoval3  49603  ackval3  49621