Definition df-3 8977

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 8969	. 2 class 3
2		c2 8968	. . 3 class 2
3		c1 7811	. . 3 class 1
4		caddc 7813	. . 3 class +
5	2, 3, 4	co 5874	. 2 class ( 2 + 1 )
6	1, 5	wceq 1353	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8991  3pos  9011  3m1e2  9037  2p2e4  9044  2p1e3  9050  3p3e6  9059  4p3e7  9061  5p3e8  9064  6p3e9  9067  3t3e9  9074  3nn  9079  2lt3  9087  7p3e10  9456  7p6e13  9459  8p3e11  9462  8p5e13  9464  9p3e12  9469  9p4e13  9470  4t3e12  9479  5t3e15  9482  6t3e18  9486  7t3e21  9491  8t3e24  9497  9t3e27  9504  nn01to3  9615  fztpval  10080  fz0to3un2pr  10120  fz0to4untppr  10121  fzo0to42pr  10217  cu2  10615  i3  10618  binom3  10634  fac3  10707  ege2le3  11674  ef4p  11697  cos1bnd  11762  3prm  12122  oddprmge3  12129  dveflem  14080  sincosq3sgn  14142  sincosq4sgn  14143  tangtx  14152  sincos6thpi  14156  binom4  14290  lgsdir2lem3  14324