Definition df-3 12116

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 12108	. 2 class 3
2		c2 12107	. . 3 class 2
3		c1 10951	. . 3 class 1
4		caddc 10953	. . 3 class +
5	2, 3, 4	co 7316	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12131  3re  12132  3cn  12133  3pos  12157  3m1e2  12180  2p2e4  12187  2p1e3  12194  3p3e6  12204  4p3e7  12206  5p3e8  12209  6p3e9  12212  3t3e9  12219  2lt3  12224  7p3e10  12591  7p6e13  12594  8p3e11  12597  8p5e13  12599  9p3e12  12604  9p4e13  12605  4t3e12  12614  5t3e15  12617  6t3e18  12621  7t3e21  12626  8t3e24  12632  9t3e27  12639  nn01to3  12760  fztpval  13397  fz0to3un2pr  13437  fz0to4untppr  13438  fzo0to42pr  13553  fzo1to4tp  13554  cu2  13996  i3  13999  binom3  14018  fac3  14073  hashtpg  14277  sqrlem7  15036  bpoly2  15843  bpoly4  15845  fsumcube  15846  ege2le3  15875  ef4p  15898  cos1bnd  15972  oddprmge3  16479  prmgaplem3  16828  13prm  16891  23prm  16894  43prm  16897  83prm  16898  163prm  16900  lt6abl  19568  cphipval  24487  vitalilem4  24855  itgcnlem  25034  dveflem  25223  sincosq3sgn  25737  sincosq4sgn  25738  tangtx  25742  sincos6thpi  25752  ang180lem2  26040  mcubic  26077  cubic2  26078  binom4  26080  dquartlem2  26082  quart1  26086  quartlem1  26087  log2ublem3  26178  basellem5  26314  basellem8  26317  basellem9  26318  ppi3  26400  cht3  26402  ppiublem1  26430  ppiublem2  26431  ppiub  26432  chtub  26440  bclbnd  26508  bposlem2  26513  bposlem9  26520  lgsdir2lem3  26555  dchrvmasumiflem1  26729  mulog2sumlem2  26763  pntlemk  26834  pntlemo  26835  axlowdimlem3  27445  axlowdimlem13  27455  axlowdimlem16  27458  axlowdimlem17  27459  2wlkdlem1  28422  elwwlks2s3  28448  elwspths2spth  28464  upgr3v3e3cycl  28676  upgr4cycl4dv4e  28681  konigsberglem5  28752  ipval2  29201  stm1add3i  30741  stadd3i  30742  problem2  33759  problem4  33761  sinccvglem  33765  mblfinlem3  35893  heiborlem6  36051  aks4d1p1  40310  2ap1caineq  40330  fac2xp3  40389  sn-0ne2  40610  3cubeslem2  40728  3cubeslem3r  40730  rmydioph  41058  rmxdioph  41060  expdiophlem2  41066  expdioph  41067  amgm3d  42049  stoweidlem26  43822  31prm  45319  lighneallem4b  45331  3odd  45430  sbgoldbo  45509  itcoval3  46281  ackval3  46299