Definition df-3 8981

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 8973	. 2 class 3
2		c2 8972	. . 3 class 2
3		c1 7814	. . 3 class 1
4		caddc 7816	. . 3 class +
5	2, 3, 4	co 5877	. 2 class ( 2 + 1 )
6	1, 5	wceq 1353	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8995  3pos  9015  3m1e2  9041  2p2e4  9048  2p1e3  9054  3p3e6  9063  4p3e7  9065  5p3e8  9068  6p3e9  9071  3t3e9  9078  3nn  9083  2lt3  9091  7p3e10  9460  7p6e13  9463  8p3e11  9466  8p5e13  9468  9p3e12  9473  9p4e13  9474  4t3e12  9483  5t3e15  9486  6t3e18  9490  7t3e21  9495  8t3e24  9501  9t3e27  9508  nn01to3  9619  fztpval  10085  fz0to3un2pr  10125  fz0to4untppr  10126  fzo0to42pr  10222  cu2  10621  i3  10624  binom3  10640  fac3  10714  ege2le3  11681  ef4p  11704  cos1bnd  11769  3prm  12130  oddprmge3  12137  dveflem  14226  sincosq3sgn  14288  sincosq4sgn  14289  tangtx  14298  sincos6thpi  14302  binom4  14436  lgsdir2lem3  14470