Definition df-3 9186

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 9178	. 2 class 3
2		c2 9177	. . 3 class 2
3		c1 8016	. . 3 class 1
4		caddc 8018	. . 3 class +
5	2, 3, 4	co 6010	. 2 class (2 + 1)
6	1, 5	wceq 1395	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9200  3pos  9220  3m1e2  9246  2p2e4  9253  2p1e3  9260  3p3e6  9269  4p3e7  9271  5p3e8  9274  6p3e9  9277  3t3e9  9284  3nn  9289  2lt3  9297  7p3e10  9668  7p6e13  9671  8p3e11  9674  8p5e13  9676  9p3e12  9681  9p4e13  9682  4t3e12  9691  5t3e15  9694  6t3e18  9698  7t3e21  9703  8t3e24  9709  9t3e27  9716  nn01to3  9829  fztpval  10296  fz0to3un2pr  10336  fz0to4untppr  10337  fzo0to42pr  10443  cu2  10877  i3  10880  binom3  10896  fac3  10971  ege2le3  12203  ef4p  12226  cos1bnd  12291  3prm  12671  oddprmge3  12678  dveflem  15421  sincosq3sgn  15523  sincosq4sgn  15524  tangtx  15533  sincos6thpi  15537  binom4  15674  lgsdir2lem3  15730