Definition df-3 8690

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 8682	. 2 class 3
2		c2 8681	. . 3 class 2
3		c1 7548	. . 3 class 1
4		caddc 7550	. . 3 class +
5	2, 3, 4	co 5728	. 2 class ( 2 + 1 )
6	1, 5	wceq 1314	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8704  3pos  8724  3m1e2  8750  2p2e4  8751  2p1e3  8757  3p3e6  8766  4p3e7  8768  5p3e8  8771  6p3e9  8774  3t3e9  8781  3nn  8786  2lt3  8794  7p3e10  9160  7p6e13  9163  8p3e11  9166  8p5e13  9168  9p3e12  9173  9p4e13  9174  4t3e12  9183  5t3e15  9186  6t3e18  9190  7t3e21  9195  8t3e24  9201  9t3e27  9208  nn01to3  9311  fztpval  9756  fzo0to42pr  9890  cu2  10284  i3  10287  binom3  10302  fac3  10371  ege2le3  11228  ef4p  11251  cos1bnd  11317  3prm  11655  oddprmge3  11661