Definition df-3 9042

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 9034	. 2 class 3
2		c2 9033	. . 3 class 2
3		c1 7873	. . 3 class 1
4		caddc 7875	. . 3 class +
5	2, 3, 4	co 5918	. 2 class (2 + 1)
6	1, 5	wceq 1364	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9056  3pos  9076  3m1e2  9102  2p2e4  9109  2p1e3  9115  3p3e6  9124  4p3e7  9126  5p3e8  9129  6p3e9  9132  3t3e9  9139  3nn  9144  2lt3  9152  7p3e10  9522  7p6e13  9525  8p3e11  9528  8p5e13  9530  9p3e12  9535  9p4e13  9536  4t3e12  9545  5t3e15  9548  6t3e18  9552  7t3e21  9557  8t3e24  9563  9t3e27  9570  nn01to3  9682  fztpval  10149  fz0to3un2pr  10189  fz0to4untppr  10190  fzo0to42pr  10287  cu2  10709  i3  10712  binom3  10728  fac3  10803  ege2le3  11814  ef4p  11837  cos1bnd  11902  3prm  12266  oddprmge3  12273  dveflem  14872  sincosq3sgn  14963  sincosq4sgn  14964  tangtx  14973  sincos6thpi  14977  binom4  15111  lgsdir2lem3  15146