Definition df-3 8993

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 8985	. 2 class 3
2		c2 8984	. . 3 class 2
3		c1 7826	. . 3 class 1
4		caddc 7828	. . 3 class +
5	2, 3, 4	co 5888	. 2 class (2 + 1)
6	1, 5	wceq 1363	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9007  3pos  9027  3m1e2  9053  2p2e4  9060  2p1e3  9066  3p3e6  9075  4p3e7  9077  5p3e8  9080  6p3e9  9083  3t3e9  9090  3nn  9095  2lt3  9103  7p3e10  9472  7p6e13  9475  8p3e11  9478  8p5e13  9480  9p3e12  9485  9p4e13  9486  4t3e12  9495  5t3e15  9498  6t3e18  9502  7t3e21  9507  8t3e24  9513  9t3e27  9520  nn01to3  9631  fztpval  10097  fz0to3un2pr  10137  fz0to4untppr  10138  fzo0to42pr  10234  cu2  10633  i3  10636  binom3  10652  fac3  10726  ege2le3  11693  ef4p  11716  cos1bnd  11781  3prm  12142  oddprmge3  12149  dveflem  14483  sincosq3sgn  14545  sincosq4sgn  14546  tangtx  14555  sincos6thpi  14559  binom4  14693  lgsdir2lem3  14727