Definition df-3 9343

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 9335	. 2 class 3
2		c2 9334	. . 3 class 2
3		c1 8170	. . 3 class 1
4		caddc 8172	. . 3 class +
5	2, 3, 4	co 6075	. 2 class (2 + 1)
6	1, 5	wceq 1402	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9357  3pos  9377  3m1e2  9403  2p2e4  9410  2p1e3  9417  3p3e6  9426  4p3e7  9428  5p3e8  9431  6p3e9  9434  3t3e9  9441  3nn  9446  2lt3  9454  7p3e10  9830  7p6e13  9833  8p3e11  9836  8p5e13  9838  9p3e12  9843  9p4e13  9844  4t3e12  9853  5t3e15  9856  6t3e18  9860  7t3e21  9865  8t3e24  9871  9t3e27  9878  nn01to3  9996  fztpval  10468  fz0to3un2pr  10508  fz0to4untppr  10509  fzo0to42pr  10616  cu2  11053  i3  11056  binom3  11072  fac3  11148  ege2le3  12416  ef4p  12439  cos1bnd  12504  3prm  12884  oddprmge3  12891  dveflem  15750  sincosq3sgn  15852  sincosq4sgn  15853  tangtx  15862  sincos6thpi  15866  binom4  16004  lgsdir2lem3  16063  konigsberglem5  16647