Definition df-3 9367

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 9359	. 2 class 3
2		c2 9358	. . 3 class 2
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 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  9381  3pos  9401  3m1e2  9427  2p2e4  9434  2p1e3  9441  3p3e6  9450  4p3e7  9452  5p3e8  9455  6p3e9  9458  3t3e9  9466  3nn  9472  2lt3  9480  7p3e10  9861  7p6e13  9864  8p3e11  9867  8p5e13  9869  9p3e12  9874  9p4e13  9875  4t3e12  9884  5t3e15  9887  6t3e18  9891  7t3e21  9896  8t3e24  9902  9t3e27  9909  nn01to3  10027  fztpval  10501  fz0to3un2pr  10541  fz0to4untppr  10542  fzo0to42pr  10649  cu2  11090  i3  11093  binom3  11109  fac3  11186  ege2le3  12457  ef4p  12480  cos1bnd  12545  3prm  12925  oddprmge3  12933  13prm  13253  23prm  13256  43prm  13259  83prm  13260  163prm  13262  dveflem  15918  sincosq3sgn  16021  sincosq4sgn  16022  tangtx  16031  sincos6thpi  16035  binom4  16180  log2ublem3  16184  ppi3  16236  cht3  16238  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  chtqub  16257  bclbnd  16268  bposlem2  16273  bposlem9  16280  lgsdir2lem3  16315  konigsberglem5  16899