Definition df-3 9067

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 9059	. 2 class 3
2		c2 9058	. . 3 class 2
3		c1 7897	. . 3 class 1
4		caddc 7899	. . 3 class +
5	2, 3, 4	co 5925	. 2 class ( 2 + 1 )
6	1, 5	wceq 1364	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9081  3pos  9101  3m1e2  9127  2p2e4  9134  2p1e3  9141  3p3e6  9150  4p3e7  9152  5p3e8  9155  6p3e9  9158  3t3e9  9165  3nn  9170  2lt3  9178  7p3e10  9548  7p6e13  9551  8p3e11  9554  8p5e13  9556  9p3e12  9561  9p4e13  9562  4t3e12  9571  5t3e15  9574  6t3e18  9578  7t3e21  9583  8t3e24  9589  9t3e27  9596  nn01to3  9708  fztpval  10175  fz0to3un2pr  10215  fz0to4untppr  10216  fzo0to42pr  10313  cu2  10747  i3  10750  binom3  10766  fac3  10841  ege2le3  11853  ef4p  11876  cos1bnd  11941  3prm  12321  oddprmge3  12328  dveflem  15046  sincosq3sgn  15148  sincosq4sgn  15149  tangtx  15158  sincos6thpi  15162  binom4  15299  lgsdir2lem3  15355