Definition df-3 9245

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 9237	. 2 class 3
2		c2 9236	. . 3 class 2
3		c1 8076	. . 3 class 1
4		caddc 8078	. . 3 class +
5	2, 3, 4	co 6028	. 2 class (2 + 1)
6	1, 5	wceq 1398	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9259  3pos  9279  3m1e2  9305  2p2e4  9312  2p1e3  9319  3p3e6  9328  4p3e7  9330  5p3e8  9333  6p3e9  9336  3t3e9  9343  3nn  9348  2lt3  9356  7p3e10  9729  7p6e13  9732  8p3e11  9735  8p5e13  9737  9p3e12  9742  9p4e13  9743  4t3e12  9752  5t3e15  9755  6t3e18  9759  7t3e21  9764  8t3e24  9770  9t3e27  9777  nn01to3  9895  fztpval  10363  fz0to3un2pr  10403  fz0to4untppr  10404  fzo0to42pr  10511  cu2  10946  i3  10949  binom3  10965  fac3  11040  ege2le3  12295  ef4p  12318  cos1bnd  12383  3prm  12763  oddprmge3  12770  dveflem  15520  sincosq3sgn  15622  sincosq4sgn  15623  tangtx  15632  sincos6thpi  15636  binom4  15773  lgsdir2lem3  15832  konigsberglem5  16416