Definition df-3 12328

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 12320	. 2 class 3
2		c2 12319	. . 3 class 2
3		c1 11159	. . 3 class 1
4		caddc 11161	. . 3 class +
5	2, 3, 4	co 7424	. 2 class (2 + 1)
6	1, 5	wceq 1534	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12343  3re  12344  3cn  12345  3pos  12369  3m1e2  12392  2p2e4  12399  2p1e3  12406  3p3e6  12416  4p3e7  12418  5p3e8  12421  6p3e9  12424  3t3e9  12431  2lt3  12436  7p3e10  12804  7p6e13  12807  8p3e11  12810  8p5e13  12812  9p3e12  12817  9p4e13  12818  4t3e12  12827  5t3e15  12830  6t3e18  12834  7t3e21  12839  8t3e24  12845  9t3e27  12852  nn01to3  12977  fztpval  13617  fz0to3un2pr  13657  fz0to4untppr  13658  fzo0to42pr  13773  fzo1to4tp  13774  cu2  14218  i3  14221  binom3  14241  fac3  14297  hashtpg  14504  01sqrexlem7  15253  bpoly2  16059  bpoly4  16061  fsumcube  16062  ege2le3  16092  ef4p  16115  cos1bnd  16189  oddprmge3  16701  prmgaplem3  17055  13prm  17118  23prm  17121  43prm  17124  83prm  17125  163prm  17127  lt6abl  19893  cphipval  25262  vitalilem4  25631  itgcnlem  25810  dveflem  26002  sincosq3sgn  26528  sincosq4sgn  26529  tangtx  26533  sincos6thpi  26543  ang180lem2  26838  mcubic  26875  cubic2  26876  binom4  26878  dquartlem2  26880  quart1  26884  quartlem1  26885  log2ublem3  26976  basellem5  27113  basellem8  27116  basellem9  27117  ppi3  27199  cht3  27201  ppiublem1  27231  ppiublem2  27232  ppiub  27233  chtub  27241  bclbnd  27309  bposlem2  27314  bposlem9  27321  lgsdir2lem3  27356  dchrvmasumiflem1  27530  mulog2sumlem2  27564  pntlemk  27635  pntlemo  27636  axlowdimlem3  28878  axlowdimlem13  28888  axlowdimlem16  28891  axlowdimlem17  28892  2wlkdlem1  29859  elwwlks2s3  29885  elwspths2spth  29901  upgr3v3e3cycl  30113  upgr4cycl4dv4e  30118  konigsberglem5  30189  ipval2  30640  stm1add3i  32180  stadd3i  32181  problem2  35494  problem4  35496  sinccvglem  35500  mblfinlem3  37360  heiborlem6  37517  aks4d1p1  41775  2ap1caineq  41843  fac2xp3  41925  nicomachus  42111  sn-0ne2  42186  3cubeslem2  42342  3cubeslem3r  42344  rmydioph  42672  rmxdioph  42674  expdiophlem2  42680  expdioph  42681  amgm3d  43866  stoweidlem26  45647  31prm  47169  lighneallem4b  47181  3odd  47280  sbgoldbo  47359  itcoval3  48053  ackval3  48071