Definition df-3 8950

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 8942	. 2 class 3
2		c2 8941	. . 3 class 2
3		c1 7787	. . 3 class 1
4		caddc 7789	. . 3 class +
5	2, 3, 4	co 5865	. 2 class (2 + 1)
6	1, 5	wceq 1353	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  8964  3pos  8984  3m1e2  9010  2p2e4  9017  2p1e3  9023  3p3e6  9032  4p3e7  9034  5p3e8  9037  6p3e9  9040  3t3e9  9047  3nn  9052  2lt3  9060  7p3e10  9429  7p6e13  9432  8p3e11  9435  8p5e13  9437  9p3e12  9442  9p4e13  9443  4t3e12  9452  5t3e15  9455  6t3e18  9459  7t3e21  9464  8t3e24  9470  9t3e27  9477  nn01to3  9588  fztpval  10051  fz0to3un2pr  10091  fz0to4untppr  10092  fzo0to42pr  10188  cu2  10586  i3  10589  binom3  10605  fac3  10678  ege2le3  11645  ef4p  11668  cos1bnd  11733  3prm  12093  oddprmge3  12100  dveflem  13738  sincosq3sgn  13800  sincosq4sgn  13801  tangtx  13810  sincos6thpi  13814  binom4  13948  lgsdir2lem3  13982