Definition df-3 11368

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 11360	. 2 class 3
2		c2 11359	. . 3 class 2
3		c1 10225	. . 3 class 1
4		caddc 10227	. . 3 class +
5	2, 3, 4	co 6877	. 2 class (2 + 1)
6	1, 5	wceq 1637	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  11381  3pos  11400  3m1e2  11423  2p2e4  11430  2p1e3  11437  3p3e6  11446  4p3e7  11448  5p3e8  11451  6p3e9  11454  3t3e9  11461  3nn  11466  2lt3  11474  7p3e10  11837  7p6e13  11840  8p3e11  11843  8p5e13  11845  9p3e12  11850  9p4e13  11851  4t3e12  11860  5t3e15  11863  6t3e18  11867  7t3e21  11872  8t3e24  11878  9t3e27  11885  nn01to3  12003  fztpval  12628  fz0to3un2pr  12668  fz0to4untppr  12669  fzo0to42pr  12782  fzo1to4tp  12783  cu2  13189  i3  13192  binom3  13211  fac3  13290  hashtpg  13487  sqrlem7  14215  bpoly2  15011  bpoly4  15013  fsumcube  15014  ege2le3  15043  ef4p  15066  cos1bnd  15140  3prm  15627  oddprmge3  15633  prmgaplem3  15977  13prm  16037  23prm  16040  43prm  16043  83prm  16044  163prm  16046  lt6abl  18500  cphipval  23258  vitalilem4  23598  iblcnlem1  23774  itgcnlem  23776  dveflem  23962  sincosq3sgn  24473  sincosq4sgn  24474  tangtx  24478  sincos6thpi  24488  ang180lem2  24760  mcubic  24794  cubic2  24795  binom4  24797  dquartlem2  24799  quart1  24803  quartlem1  24804  log2ublem3  24895  basellem5  25031  basellem8  25034  basellem9  25035  ppi3  25117  cht3  25119  ppiublem1  25147  ppiublem2  25148  ppiub  25149  chtub  25157  bclbnd  25225  bposlem2  25230  bposlem9  25237  lgsdir2lem3  25272  dchrvmasumiflem1  25410  mulog2sumlem2  25444  pntlemk  25515  pntlemo  25516  axlowdimlem3  26044  axlowdimlem13  26054  axlowdimlem16  26057  axlowdimlem17  26058  2wlkdlem1  27071  elwwlks2s3  27097  elwspths2spth  27115  upgr3v3e3cycl  27359  upgr4cycl4dv4e  27364  konigsberglem5  27435  ipval2  27896  stm1add3i  29440  stadd3i  29441  problem2  31887  problem4  31889  sinccvglem  31893  mblfinlem3  33763  heiborlem6  33928  rmydioph  38083  rmxdioph  38085  expdiophlem2  38091  expdioph  38092  amgm3d  39003  stoweidlem26  40723  31prm  42088  lighneallem4b  42102  3odd  42193  sbgoldbo  42251