Definition df-3 9346

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 9338	. 2 class 3
2		c2 9337	. . 3 class 2
3		c1 8173	. . 3 class 1
4		caddc 8175	. . 3 class +
5	2, 3, 4	co 6078	. 2 class ( 2 + 1 )
6	1, 5	wceq 1402	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9360  3pos  9380  3m1e2  9406  2p2e4  9413  2p1e3  9420  3p3e6  9429  4p3e7  9431  5p3e8  9434  6p3e9  9437  3t3e9  9444  3nn  9449  2lt3  9457  7p3e10  9833  7p6e13  9836  8p3e11  9839  8p5e13  9841  9p3e12  9846  9p4e13  9847  4t3e12  9856  5t3e15  9859  6t3e18  9863  7t3e21  9868  8t3e24  9874  9t3e27  9881  nn01to3  9999  fztpval  10471  fz0to3un2pr  10511  fz0to4untppr  10512  fzo0to42pr  10619  cu2  11056  i3  11059  binom3  11075  fac3  11151  ege2le3  12419  ef4p  12442  cos1bnd  12507  3prm  12887  oddprmge3  12894  dveflem  15753  sincosq3sgn  15855  sincosq4sgn  15856  tangtx  15865  sincos6thpi  15869  binom4  16007  lgsdir2lem3  16066  konigsberglem5  16650