Definition df-3 8917

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 8909	. 2 class 3
2		c2 8908	. . 3 class 2
3		c1 7754	. . 3 class 1
4		caddc 7756	. . 3 class +
5	2, 3, 4	co 5842	. 2 class (2 + 1)
6	1, 5	wceq 1343	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  8931  3pos  8951  3m1e2  8977  2p2e4  8984  2p1e3  8990  3p3e6  8999  4p3e7  9001  5p3e8  9004  6p3e9  9007  3t3e9  9014  3nn  9019  2lt3  9027  7p3e10  9396  7p6e13  9399  8p3e11  9402  8p5e13  9404  9p3e12  9409  9p4e13  9410  4t3e12  9419  5t3e15  9422  6t3e18  9426  7t3e21  9431  8t3e24  9437  9t3e27  9444  nn01to3  9555  fztpval  10018  fz0to3un2pr  10058  fz0to4untppr  10059  fzo0to42pr  10155  cu2  10553  i3  10556  binom3  10572  fac3  10645  ege2le3  11612  ef4p  11635  cos1bnd  11700  3prm  12060  oddprmge3  12067  dveflem  13327  sincosq3sgn  13389  sincosq4sgn  13390  tangtx  13399  sincos6thpi  13403  binom4  13537  lgsdir2lem3  13571