Definition df-3 12037

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 12029	. 2 class 3
2		c2 12028	. . 3 class 2
3		c1 10872	. . 3 class 1
4		caddc 10874	. . 3 class +
5	2, 3, 4	co 7275	. 2 class (2 + 1)
6	1, 5	wceq 1539	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12052  3re  12053  3cn  12054  3pos  12078  3m1e2  12101  2p2e4  12108  2p1e3  12115  3p3e6  12125  4p3e7  12127  5p3e8  12130  6p3e9  12133  3t3e9  12140  2lt3  12145  7p3e10  12512  7p6e13  12515  8p3e11  12518  8p5e13  12520  9p3e12  12525  9p4e13  12526  4t3e12  12535  5t3e15  12538  6t3e18  12542  7t3e21  12547  8t3e24  12553  9t3e27  12560  nn01to3  12681  fztpval  13318  fz0to3un2pr  13358  fz0to4untppr  13359  fzo0to42pr  13474  fzo1to4tp  13475  cu2  13917  i3  13920  binom3  13939  fac3  13994  hashtpg  14199  sqrlem7  14960  bpoly2  15767  bpoly4  15769  fsumcube  15770  ege2le3  15799  ef4p  15822  cos1bnd  15896  oddprmge3  16405  prmgaplem3  16754  13prm  16817  23prm  16820  43prm  16823  83prm  16824  163prm  16826  lt6abl  19496  cphipval  24407  vitalilem4  24775  itgcnlem  24954  dveflem  25143  sincosq3sgn  25657  sincosq4sgn  25658  tangtx  25662  sincos6thpi  25672  ang180lem2  25960  mcubic  25997  cubic2  25998  binom4  26000  dquartlem2  26002  quart1  26006  quartlem1  26007  log2ublem3  26098  basellem5  26234  basellem8  26237  basellem9  26238  ppi3  26320  cht3  26322  ppiublem1  26350  ppiublem2  26351  ppiub  26352  chtub  26360  bclbnd  26428  bposlem2  26433  bposlem9  26440  lgsdir2lem3  26475  dchrvmasumiflem1  26649  mulog2sumlem2  26683  pntlemk  26754  pntlemo  26755  axlowdimlem3  27312  axlowdimlem13  27322  axlowdimlem16  27325  axlowdimlem17  27326  2wlkdlem1  28290  elwwlks2s3  28316  elwspths2spth  28332  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  konigsberglem5  28620  ipval2  29069  stm1add3i  30609  stadd3i  30610  problem2  33624  problem4  33626  sinccvglem  33630  mblfinlem3  35816  heiborlem6  35974  aks4d1p1  40084  2ap1caineq  40101  fac2xp3  40160  sn-0ne2  40389  3cubeslem2  40507  3cubeslem3r  40509  rmydioph  40836  rmxdioph  40838  expdiophlem2  40844  expdioph  40845  amgm3d  41810  stoweidlem26  43567  31prm  45049  lighneallem4b  45061  3odd  45160  sbgoldbo  45239  itcoval3  46011  ackval3  46029