Definition df-3 9314

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 9306	. 2 class 3
2		c2 9305	. . 3 class 2
3		c1 8144	. . 3 class 1
4		caddc 8146	. . 3 class +
5	2, 3, 4	co 6058	. 2 class (2 + 1)
6	1, 5	wceq 1398	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9328  3pos  9348  3m1e2  9374  2p2e4  9381  2p1e3  9388  3p3e6  9397  4p3e7  9399  5p3e8  9402  6p3e9  9405  3t3e9  9412  3nn  9417  2lt3  9425  7p3e10  9801  7p6e13  9804  8p3e11  9807  8p5e13  9809  9p3e12  9814  9p4e13  9815  4t3e12  9824  5t3e15  9827  6t3e18  9831  7t3e21  9836  8t3e24  9842  9t3e27  9849  nn01to3  9967  fztpval  10439  fz0to3un2pr  10479  fz0to4untppr  10480  fzo0to42pr  10587  cu2  11024  i3  11027  binom3  11043  fac3  11119  ege2le3  12382  ef4p  12405  cos1bnd  12470  3prm  12850  oddprmge3  12857  dveflem  15717  sincosq3sgn  15819  sincosq4sgn  15820  tangtx  15829  sincos6thpi  15833  binom4  15970  lgsdir2lem3  16029  konigsberglem5  16613