Definition df-3 12240

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 12232	. 2 class 3
2		c2 12231	. . 3 class 2
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (2 + 1)
6	1, 5	wceq 1548	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12255  3re  12256  3cn  12257  3pos  12281  3m1e2  12299  2p2e4  12306  2p1e3  12313  3p3e6  12323  4p3e7  12325  5p3e8  12328  6p3e9  12331  3t3e9  12338  2lt3  12343  7p3e10  12714  7p6e13  12717  8p3e11  12720  8p5e13  12722  9p3e12  12727  9p4e13  12728  4t3e12  12737  5t3e15  12740  6t3e18  12744  7t3e21  12749  8t3e24  12755  9t3e27  12762  nn01to3  12886  fztpval  13535  fz0to3un2pr  13578  fzo0to42pr  13703  fzo1to4tp  13704  cu2  14157  i3  14160  binom3  14181  fac3  14237  hashtpg  14442  01sqrexlem7  15205  bpoly2  16017  bpoly4  16019  fsumcube  16020  ege2le3  16050  ef4p  16075  cos1bnd  16149  oddprmge3  16665  prmgaplem3  17019  13prm  17081  23prm  17084  43prm  17087  83prm  17088  163prm  17090  lt6abl  19864  cphipval  25231  vitalilem4  25599  itgcnlem  25778  dveflem  25967  sincosq3sgn  26485  sincosq4sgn  26486  tangtx  26490  sincos6thpi  26501  ang180lem2  26795  mcubic  26832  cubic2  26833  binom4  26835  dquartlem2  26837  quart1  26841  quartlem1  26842  log2ublem3  26933  basellem5  27069  basellem8  27072  basellem9  27073  ppi3  27155  cht3  27157  ppiublem1  27186  ppiublem2  27187  ppiub  27188  chtub  27196  bclbnd  27264  bposlem2  27269  bposlem9  27276  lgsdir2lem3  27311  dchrvmasumiflem1  27485  mulog2sumlem2  27519  pntlemk  27590  pntlemo  27591  axlowdimlem3  29033  axlowdimlem13  29043  axlowdimlem16  29046  axlowdimlem17  29047  2wlkdlem1  30013  elwwlks2s3  30039  elwspths2spth  30058  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  konigsberglem5  30346  ipval2  30798  stm1add3i  32338  stadd3i  32339  problem2  35907  problem4  35909  sinccvglem  35913  mblfinlem3  38039  heiborlem6  38196  aks4d1p1  42574  2ap1caineq  42643  1p3e4  42755  nicomachus  42802  sn-0ne2  42896  3cubeslem2  43147  3cubeslem3r  43149  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  expdioph  43481  amgm3d  44656  stoweidlem26  46481  sin3t  47346  cos3t  47347  sin5tlem1  47348  2timesltsq  47853  2timesltsqm1  47854  31prm  48087  lighneallem4b  48099  nprmdvdsfacm1lem2  48111  3odd  48211  sbgoldbo  48290  itcoval3  49168  ackval3  49186