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  9866  7p6e13  9869  8p3e11  9872  8p5e13  9874  9p3e12  9879  9p4e13  9880  4t3e12  9889  5t3e15  9892  6t3e18  9896  7t3e21  9901  8t3e24  9907  9t3e27  9914  nn01to3  10032  fztpval  10506  fz0to3un2pr  10546  fz0to4untppr  10547  fzo0to42pr  10654  cu2  11095  i3  11098  binom3  11114  fac3  11191  ege2le3  12462  ef4p  12485  cos1bnd  12550  3prm  12930  oddprmge3  12938  13prm  13258  23prm  13261  43prm  13264  83prm  13265  163prm  13267  dveflem  15969  sincosq3sgn  16072  sincosq4sgn  16073  tangtx  16082  sincos6thpi  16086  binom4  16236  log2ublem3  16240  ppi3  16292  cht3  16294  ppiublem1  16308  ppiublem2  16309  ppiqub  16310  chtqub  16313  bclbnd  16324  bposlem2  16329  bposlem9  16336  lgsdir2lem3  16371  konigsberglem5  16955