Definition df-3 9098

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 9090	. 2 class 3
2		c2 9089	. . 3 class 2
3		c1 7928	. . 3 class 1
4		caddc 7930	. . 3 class +
5	2, 3, 4	co 5946	. 2 class ( 2 + 1 )
6	1, 5	wceq 1373	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9112  3pos  9132  3m1e2  9158  2p2e4  9165  2p1e3  9172  3p3e6  9181  4p3e7  9183  5p3e8  9186  6p3e9  9189  3t3e9  9196  3nn  9201  2lt3  9209  7p3e10  9580  7p6e13  9583  8p3e11  9586  8p5e13  9588  9p3e12  9593  9p4e13  9594  4t3e12  9603  5t3e15  9606  6t3e18  9610  7t3e21  9615  8t3e24  9621  9t3e27  9628  nn01to3  9740  fztpval  10207  fz0to3un2pr  10247  fz0to4untppr  10248  fzo0to42pr  10351  cu2  10785  i3  10788  binom3  10804  fac3  10879  ege2le3  12015  ef4p  12038  cos1bnd  12103  3prm  12483  oddprmge3  12490  dveflem  15231  sincosq3sgn  15333  sincosq4sgn  15334  tangtx  15343  sincos6thpi  15347  binom4  15484  lgsdir2lem3  15540