Definition df-3 9044

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 9036	. 2 class 3
2		c2 9035	. . 3 class 2
3		c1 7875	. . 3 class 1
4		caddc 7877	. . 3 class +
5	2, 3, 4	co 5919	. 2 class (2 + 1)
6	1, 5	wceq 1364	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9058  3pos  9078  3m1e2  9104  2p2e4  9111  2p1e3  9118  3p3e6  9127  4p3e7  9129  5p3e8  9132  6p3e9  9135  3t3e9  9142  3nn  9147  2lt3  9155  7p3e10  9525  7p6e13  9528  8p3e11  9531  8p5e13  9533  9p3e12  9538  9p4e13  9539  4t3e12  9548  5t3e15  9551  6t3e18  9555  7t3e21  9560  8t3e24  9566  9t3e27  9573  nn01to3  9685  fztpval  10152  fz0to3un2pr  10192  fz0to4untppr  10193  fzo0to42pr  10290  cu2  10712  i3  10715  binom3  10731  fac3  10806  ege2le3  11817  ef4p  11840  cos1bnd  11905  3prm  12269  oddprmge3  12276  dveflem  14905  sincosq3sgn  15004  sincosq4sgn  15005  tangtx  15014  sincos6thpi  15018  binom4  15152  lgsdir2lem3  15187