Definition df-3 9069

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 9061	. 2 class 3
2		c2 9060	. . 3 class 2
3		c1 7899	. . 3 class 1
4		caddc 7901	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (2 + 1)
6	1, 5	wceq 1364	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9083  3pos  9103  3m1e2  9129  2p2e4  9136  2p1e3  9143  3p3e6  9152  4p3e7  9154  5p3e8  9157  6p3e9  9160  3t3e9  9167  3nn  9172  2lt3  9180  7p3e10  9550  7p6e13  9553  8p3e11  9556  8p5e13  9558  9p3e12  9563  9p4e13  9564  4t3e12  9573  5t3e15  9576  6t3e18  9580  7t3e21  9585  8t3e24  9591  9t3e27  9598  nn01to3  9710  fztpval  10177  fz0to3un2pr  10217  fz0to4untppr  10218  fzo0to42pr  10315  cu2  10749  i3  10752  binom3  10768  fac3  10843  ege2le3  11855  ef4p  11878  cos1bnd  11943  3prm  12323  oddprmge3  12330  dveflem  15070  sincosq3sgn  15172  sincosq4sgn  15173  tangtx  15182  sincos6thpi  15186  binom4  15323  lgsdir2lem3  15379