Definition df-3 8978

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 8970	. 2 class 3
2		c2 8969	. . 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  8992  3pos  9012  3m1e2  9038  2p2e4  9045  2p1e3  9051  3p3e6  9060  4p3e7  9062  5p3e8  9065  6p3e9  9068  3t3e9  9075  3nn  9080  2lt3  9088  7p3e10  9457  7p6e13  9460  8p3e11  9463  8p5e13  9465  9p3e12  9470  9p4e13  9471  4t3e12  9480  5t3e15  9483  6t3e18  9487  7t3e21  9492  8t3e24  9498  9t3e27  9505  nn01to3  9616  fztpval  10082  fz0to3un2pr  10122  fz0to4untppr  10123  fzo0to42pr  10219  cu2  10618  i3  10621  binom3  10637  fac3  10711  ege2le3  11678  ef4p  11701  cos1bnd  11766  3prm  12127  oddprmge3  12134  dveflem  14157  sincosq3sgn  14219  sincosq4sgn  14220  tangtx  14229  sincos6thpi  14233  binom4  14367  lgsdir2lem3  14401