Definition df-3 9297

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 9289	. 2 class 3
2		c2 9288	. . 3 class 2
3		c1 8128	. . 3 class 1
4		caddc 8130	. . 3 class +
5	2, 3, 4	co 6050	. 2 class (2 + 1)
6	1, 5	wceq 1398	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9311  3pos  9331  3m1e2  9357  2p2e4  9364  2p1e3  9371  3p3e6  9380  4p3e7  9382  5p3e8  9385  6p3e9  9388  3t3e9  9395  3nn  9400  2lt3  9408  7p3e10  9783  7p6e13  9786  8p3e11  9789  8p5e13  9791  9p3e12  9796  9p4e13  9797  4t3e12  9806  5t3e15  9809  6t3e18  9813  7t3e21  9818  8t3e24  9824  9t3e27  9831  nn01to3  9949  fztpval  10417  fz0to3un2pr  10457  fz0to4untppr  10458  fzo0to42pr  10565  cu2  11000  i3  11003  binom3  11019  fac3  11094  ege2le3  12357  ef4p  12380  cos1bnd  12445  3prm  12825  oddprmge3  12832  dveflem  15591  sincosq3sgn  15693  sincosq4sgn  15694  tangtx  15703  sincos6thpi  15707  binom4  15844  lgsdir2lem3  15903  konigsberglem5  16487