Definition df-3 9299

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 9291	. 2 class 3
2		c2 9290	. . 3 class 2
3		c1 8130	. . 3 class 1
4		caddc 8132	. . 3 class +
5	2, 3, 4	co 6052	. 2 class ( 2 + 1 )
6	1, 5	wceq 1398	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9313  3pos  9333  3m1e2  9359  2p2e4  9366  2p1e3  9373  3p3e6  9382  4p3e7  9384  5p3e8  9387  6p3e9  9390  3t3e9  9397  3nn  9402  2lt3  9410  7p3e10  9786  7p6e13  9789  8p3e11  9792  8p5e13  9794  9p3e12  9799  9p4e13  9800  4t3e12  9809  5t3e15  9812  6t3e18  9816  7t3e21  9821  8t3e24  9827  9t3e27  9834  nn01to3  9952  fztpval  10421  fz0to3un2pr  10461  fz0to4untppr  10462  fzo0to42pr  10569  cu2  11004  i3  11007  binom3  11023  fac3  11098  ege2le3  12361  ef4p  12384  cos1bnd  12449  3prm  12829  oddprmge3  12836  dveflem  15608  sincosq3sgn  15710  sincosq4sgn  15711  tangtx  15720  sincos6thpi  15724  binom4  15861  lgsdir2lem3  15920  konigsberglem5  16504