Definition df-3 12213

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 12205	. 2 class 3
2		c2 12204	. . 3 class 2
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12228  3re  12229  3cn  12230  3pos  12254  3m1e2  12272  2p2e4  12279  2p1e3  12286  3p3e6  12296  4p3e7  12298  5p3e8  12301  6p3e9  12304  3t3e9  12311  2lt3  12316  7p3e10  12686  7p6e13  12689  8p3e11  12692  8p5e13  12694  9p3e12  12699  9p4e13  12700  4t3e12  12709  5t3e15  12712  6t3e18  12716  7t3e21  12721  8t3e24  12727  9t3e27  12734  nn01to3  12858  fztpval  13506  fz0to3un2pr  13549  fzo0to42pr  13673  fzo1to4tp  13674  cu2  14127  i3  14130  binom3  14151  fac3  14207  hashtpg  14412  01sqrexlem7  15175  bpoly2  15984  bpoly4  15986  fsumcube  15987  ege2le3  16017  ef4p  16042  cos1bnd  16116  oddprmge3  16631  prmgaplem3  16985  13prm  17047  23prm  17050  43prm  17053  83prm  17054  163prm  17056  lt6abl  19828  cphipval  25203  vitalilem4  25572  itgcnlem  25751  dveflem  25943  sincosq3sgn  26469  sincosq4sgn  26470  tangtx  26474  sincos6thpi  26485  ang180lem2  26780  mcubic  26817  cubic2  26818  binom4  26820  dquartlem2  26822  quart1  26826  quartlem1  26827  log2ublem3  26918  basellem5  27055  basellem8  27058  basellem9  27059  ppi3  27141  cht3  27143  ppiublem1  27173  ppiublem2  27174  ppiub  27175  chtub  27183  bclbnd  27251  bposlem2  27256  bposlem9  27263  lgsdir2lem3  27298  dchrvmasumiflem1  27472  mulog2sumlem2  27506  pntlemk  27577  pntlemo  27578  axlowdimlem3  29021  axlowdimlem13  29031  axlowdimlem16  29034  axlowdimlem17  29035  2wlkdlem1  30002  elwwlks2s3  30028  elwspths2spth  30047  upgr3v3e3cycl  30259  upgr4cycl4dv4e  30264  konigsberglem5  30335  ipval2  30786  stm1add3i  32326  stadd3i  32327  problem2  35862  problem4  35864  sinccvglem  35868  mblfinlem3  37862  heiborlem6  38019  aks4d1p1  42398  2ap1caineq  42467  1p3e4  42581  nicomachus  42634  sn-0ne2  42728  3cubeslem2  42994  3cubeslem3r  42996  rmydioph  43323  rmxdioph  43325  expdiophlem2  43331  expdioph  43332  amgm3d  44507  stoweidlem26  46337  31prm  47910  lighneallem4b  47922  3odd  48021  sbgoldbo  48100  itcoval3  48978  ackval3  48996