Definition df-3 9366

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 9358	. 2 class 3
2		c2 9357	. . 3 class 2
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 2 + 1 )
6	1, 5	wceq 1402	1 wff 3 = ( 2 + 1 )

This definition is used by:  3re  9380  3pos  9400  3m1e2  9426  2p2e4  9433  2p1e3  9440  3p3e6  9449  4p3e7  9451  5p3e8  9454  6p3e9  9457  3t3e9  9465  3nn  9471  2lt3  9479  7p3e10  9860  7p6e13  9863  8p3e11  9866  8p5e13  9868  9p3e12  9873  9p4e13  9874  4t3e12  9883  5t3e15  9886  6t3e18  9890  7t3e21  9895  8t3e24  9901  9t3e27  9908  nn01to3  10026  fztpval  10500  fz0to3un2pr  10540  fz0to4untppr  10541  fzo0to42pr  10648  cu2  11088  i3  11091  binom3  11107  fac3  11184  ege2le3  12454  ef4p  12477  cos1bnd  12542  3prm  12922  oddprmge3  12930  13prm  13250  23prm  13253  43prm  13256  83prm  13257  163prm  13259  dveflem  15876  sincosq3sgn  15979  sincosq4sgn  15980  tangtx  15989  sincos6thpi  15993  binom4  16138  log2ublem3  16142  ppi3  16180  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  bclbnd  16205  bposlem2  16210  lgsdir2lem3  16247  konigsberglem5  16831