Definition df-3 9262

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 9254	. 2 class 3
2		c2 9253	. . 3 class 2
3		c1 8093	. . 3 class 1
4		caddc 8095	. . 3 class +
5	2, 3, 4	co 6028	. 2 class ( 2 + 1 )
6	1, 5	wceq 1398	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9276  3pos  9296  3m1e2  9322  2p2e4  9329  2p1e3  9336  3p3e6  9345  4p3e7  9347  5p3e8  9350  6p3e9  9353  3t3e9  9360  3nn  9365  2lt3  9373  7p3e10  9746  7p6e13  9749  8p3e11  9752  8p5e13  9754  9p3e12  9759  9p4e13  9760  4t3e12  9769  5t3e15  9772  6t3e18  9776  7t3e21  9781  8t3e24  9787  9t3e27  9794  nn01to3  9912  fztpval  10380  fz0to3un2pr  10420  fz0to4untppr  10421  fzo0to42pr  10528  cu2  10963  i3  10966  binom3  10982  fac3  11057  ege2le3  12312  ef4p  12335  cos1bnd  12400  3prm  12780  oddprmge3  12787  dveflem  15537  sincosq3sgn  15639  sincosq4sgn  15640  tangtx  15649  sincos6thpi  15653  binom4  15790  lgsdir2lem3  15849  konigsberglem5  16433