Definition df-3 9373

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 9365	. 2 class 3
2		c2 9364	. . 3 class 2
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 2 + 1 )
6	1, 5	wceq 1402	1 wff 3 = ( 2 + 1 )

This definition is used by:  3re  9387  3pos  9407  3m1e2  9433  2p2e4  9440  2p1e3  9447  3p3e6  9456  4p3e7  9458  5p3e8  9461  6p3e9  9464  3t3e9  9472  3nn  9478  2lt3  9486  7p3e10  9867  7p6e13  9870  8p3e11  9873  8p5e13  9875  9p3e12  9880  9p4e13  9881  4t3e12  9890  5t3e15  9893  6t3e18  9897  7t3e21  9902  8t3e24  9908  9t3e27  9915  nn01to3  10033  fztpval  10507  fz0to3un2pr  10547  fz0to4untppr  10548  fzo0to42pr  10655  cu2  11096  i3  11099  binom3  11115  fac3  11192  ege2le3  12463  ef4p  12486  cos1bnd  12551  3prm  12931  oddprmge3  12939  13prm  13259  23prm  13262  43prm  13265  83prm  13266  163prm  13268  dveflem  15952  sincosq3sgn  16055  sincosq4sgn  16056  tangtx  16065  sincos6thpi  16069  binom4  16219  log2ublem3  16223  ppi3  16275  cht3  16277  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  chtqub  16296  bclbnd  16307  bposlem2  16312  bposlem9  16319  lgsdir2lem3  16354  konigsberglem5  16938