Definition df-3 9166

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 9158	. 2 class 3
2		c2 9157	. . 3 class 2
3		c1 7996	. . 3 class 1
4		caddc 7998	. . 3 class +
5	2, 3, 4	co 6000	. 2 class (2 + 1)
6	1, 5	wceq 1395	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9180  3pos  9200  3m1e2  9226  2p2e4  9233  2p1e3  9240  3p3e6  9249  4p3e7  9251  5p3e8  9254  6p3e9  9257  3t3e9  9264  3nn  9269  2lt3  9277  7p3e10  9648  7p6e13  9651  8p3e11  9654  8p5e13  9656  9p3e12  9661  9p4e13  9662  4t3e12  9671  5t3e15  9674  6t3e18  9678  7t3e21  9683  8t3e24  9689  9t3e27  9696  nn01to3  9808  fztpval  10275  fz0to3un2pr  10315  fz0to4untppr  10316  fzo0to42pr  10421  cu2  10855  i3  10858  binom3  10874  fac3  10949  ege2le3  12177  ef4p  12200  cos1bnd  12265  3prm  12645  oddprmge3  12652  dveflem  15394  sincosq3sgn  15496  sincosq4sgn  15497  tangtx  15506  sincos6thpi  15510  binom4  15647  lgsdir2lem3  15703