Definition df-3 8979

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 8971	. 2 class 3
2		c2 8970	. . 3 class 2
3		c1 7812	. . 3 class 1
4		caddc 7814	. . 3 class +
5	2, 3, 4	co 5875	. 2 class (2 + 1)
6	1, 5	wceq 1353	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  8993  3pos  9013  3m1e2  9039  2p2e4  9046  2p1e3  9052  3p3e6  9061  4p3e7  9063  5p3e8  9066  6p3e9  9069  3t3e9  9076  3nn  9081  2lt3  9089  7p3e10  9458  7p6e13  9461  8p3e11  9464  8p5e13  9466  9p3e12  9471  9p4e13  9472  4t3e12  9481  5t3e15  9484  6t3e18  9488  7t3e21  9493  8t3e24  9499  9t3e27  9506  nn01to3  9617  fztpval  10083  fz0to3un2pr  10123  fz0to4untppr  10124  fzo0to42pr  10220  cu2  10619  i3  10622  binom3  10638  fac3  10712  ege2le3  11679  ef4p  11702  cos1bnd  11767  3prm  12128  oddprmge3  12135  dveflem  14190  sincosq3sgn  14252  sincosq4sgn  14253  tangtx  14262  sincos6thpi  14266  binom4  14400  lgsdir2lem3  14434