Definition df-3 8099

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 8090	. 2 class 3
2		c2 8089	. . 3 class 2
3		c1 6982	. . 3 class 1
4		caddc 6984	. . 3 class +
5	2, 3, 4	co 5532	. 2 class ( 2 + 1 )
6	1, 5	wceq 1284	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8113  3pos  8133  3m1e2  8158  2p2e4  8159  2p1e3  8165  3p3e6  8174  4p3e7  8176  5p3e8  8179  6p3e9  8182  3t3e9  8189  3nn  8194  2lt3  8202  7p3e10  8551  7p6e13  8554  8p3e11  8557  8p5e13  8559  9p3e12  8564  9p4e13  8565  4t3e12  8574  5t3e15  8577  6t3e18  8581  7t3e21  8586  8t3e24  8592  9t3e27  8599  nn01to3  8702  fztpval  9100  fzo0to42pr  9229  cu2  9573  i3  9576  binom3  9590  fac3  9659  3prm  10510  oddprmge3  10516