Definition df-3 8780

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 8772	. 2 class 3
2		c2 8771	. . 3 class 2
3		c1 7621	. . 3 class 1
4		caddc 7623	. . 3 class +
5	2, 3, 4	co 5774	. 2 class ( 2 + 1 )
6	1, 5	wceq 1331	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8794  3pos  8814  3m1e2  8840  2p2e4  8847  2p1e3  8853  3p3e6  8862  4p3e7  8864  5p3e8  8867  6p3e9  8870  3t3e9  8877  3nn  8882  2lt3  8890  7p3e10  9256  7p6e13  9259  8p3e11  9262  8p5e13  9264  9p3e12  9269  9p4e13  9270  4t3e12  9279  5t3e15  9282  6t3e18  9286  7t3e21  9291  8t3e24  9297  9t3e27  9304  nn01to3  9409  fztpval  9863  fzo0to42pr  9997  cu2  10391  i3  10394  binom3  10409  fac3  10478  ege2le3  11377  ef4p  11400  cos1bnd  11466  3prm  11809  oddprmge3  11815  dveflem  12855  sincosq3sgn  12909  sincosq4sgn  12910  tangtx  12919  sincos6thpi  12923