Definition df-3 9203

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 9195	. 2 class 3
2		c2 9194	. . 3 class 2
3		c1 8033	. . 3 class 1
4		caddc 8035	. . 3 class +
5	2, 3, 4	co 6018	. 2 class ( 2 + 1 )
6	1, 5	wceq 1397	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9217  3pos  9237  3m1e2  9263  2p2e4  9270  2p1e3  9277  3p3e6  9286  4p3e7  9288  5p3e8  9291  6p3e9  9294  3t3e9  9301  3nn  9306  2lt3  9314  7p3e10  9685  7p6e13  9688  8p3e11  9691  8p5e13  9693  9p3e12  9698  9p4e13  9699  4t3e12  9708  5t3e15  9711  6t3e18  9715  7t3e21  9720  8t3e24  9726  9t3e27  9733  nn01to3  9851  fztpval  10318  fz0to3un2pr  10358  fz0to4untppr  10359  fzo0to42pr  10465  cu2  10900  i3  10903  binom3  10919  fac3  10994  ege2le3  12233  ef4p  12256  cos1bnd  12321  3prm  12701  oddprmge3  12708  dveflem  15452  sincosq3sgn  15554  sincosq4sgn  15555  tangtx  15564  sincos6thpi  15568  binom4  15705  lgsdir2lem3  15761