Definition df-3 11689

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 11681	. 2 class 3
2		c2 11680	. . 3 class 2
3		c1 10527	. . 3 class 1
4		caddc 10529	. . 3 class +
5	2, 3, 4	co 7135	. 2 class (2 + 1)
6	1, 5	wceq 1538	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  11704  3re  11705  3cn  11706  3pos  11730  3m1e2  11753  2p2e4  11760  2p1e3  11767  3p3e6  11777  4p3e7  11779  5p3e8  11782  6p3e9  11785  3t3e9  11792  2lt3  11797  7p3e10  12161  7p6e13  12164  8p3e11  12167  8p5e13  12169  9p3e12  12174  9p4e13  12175  4t3e12  12184  5t3e15  12187  6t3e18  12191  7t3e21  12196  8t3e24  12202  9t3e27  12209  nn01to3  12329  fztpval  12964  fz0to3un2pr  13004  fz0to4untppr  13005  fzo0to42pr  13119  fzo1to4tp  13120  cu2  13559  i3  13562  binom3  13581  fac3  13636  hashtpg  13839  sqrlem7  14600  bpoly2  15403  bpoly4  15405  fsumcube  15406  ege2le3  15435  ef4p  15458  cos1bnd  15532  oddprmge3  16034  prmgaplem3  16379  13prm  16441  23prm  16444  43prm  16447  83prm  16448  163prm  16450  lt6abl  19008  cphipval  23847  vitalilem4  24215  itgcnlem  24393  dveflem  24582  sincosq3sgn  25093  sincosq4sgn  25094  tangtx  25098  sincos6thpi  25108  ang180lem2  25396  mcubic  25433  cubic2  25434  binom4  25436  dquartlem2  25438  quart1  25442  quartlem1  25443  log2ublem3  25534  basellem5  25670  basellem8  25673  basellem9  25674  ppi3  25756  cht3  25758  ppiublem1  25786  ppiublem2  25787  ppiub  25788  chtub  25796  bclbnd  25864  bposlem2  25869  bposlem9  25876  lgsdir2lem3  25911  dchrvmasumiflem1  26085  mulog2sumlem2  26119  pntlemk  26190  pntlemo  26191  axlowdimlem3  26738  axlowdimlem13  26748  axlowdimlem16  26751  axlowdimlem17  26752  2wlkdlem1  27711  elwwlks2s3  27737  elwspths2spth  27753  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  konigsberglem5  28041  ipval2  28490  stm1add3i  30030  stadd3i  30031  problem2  33022  problem4  33024  sinccvglem  33028  mblfinlem3  35096  heiborlem6  35254  2ap1caineq  39349  fac2xp3  39385  sn-0ne2  39544  3cubeslem2  39626  3cubeslem3r  39628  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  amgm3d  40905  stoweidlem26  42668  31prm  44114  lighneallem4b  44127  3odd  44226  sbgoldbo  44305  itcoval3  45079  ackval3  45097