Definition df-3 9050

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 9042	. 2 class 3
2		c2 9041	. . 3 class 2
3		c1 7880	. . 3 class 1
4		caddc 7882	. . 3 class +
5	2, 3, 4	co 5922	. 2 class ( 2 + 1 )
6	1, 5	wceq 1364	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9064  3pos  9084  3m1e2  9110  2p2e4  9117  2p1e3  9124  3p3e6  9133  4p3e7  9135  5p3e8  9138  6p3e9  9141  3t3e9  9148  3nn  9153  2lt3  9161  7p3e10  9531  7p6e13  9534  8p3e11  9537  8p5e13  9539  9p3e12  9544  9p4e13  9545  4t3e12  9554  5t3e15  9557  6t3e18  9561  7t3e21  9566  8t3e24  9572  9t3e27  9579  nn01to3  9691  fztpval  10158  fz0to3un2pr  10198  fz0to4untppr  10199  fzo0to42pr  10296  cu2  10730  i3  10733  binom3  10749  fac3  10824  ege2le3  11836  ef4p  11859  cos1bnd  11924  3prm  12296  oddprmge3  12303  dveflem  14962  sincosq3sgn  15064  sincosq4sgn  15065  tangtx  15074  sincos6thpi  15078  binom4  15215  lgsdir2lem3  15271