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  10466  cu2  10901  i3  10904  binom3  10920  fac3  10995  ege2le3  12250  ef4p  12273  cos1bnd  12338  3prm  12718  oddprmge3  12725  dveflem  15469  sincosq3sgn  15571  sincosq4sgn  15572  tangtx  15581  sincos6thpi  15585  binom4  15722  lgsdir2lem3  15778  konigsberglem5  16362