Definition df-3 9193

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 9185	. 2 class 3
2		c2 9184	. . 3 class 2
3		c1 8023	. . 3 class 1
4		caddc 8025	. . 3 class +
5	2, 3, 4	co 6013	. 2 class (2 + 1)
6	1, 5	wceq 1395	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9207  3pos  9227  3m1e2  9253  2p2e4  9260  2p1e3  9267  3p3e6  9276  4p3e7  9278  5p3e8  9281  6p3e9  9284  3t3e9  9291  3nn  9296  2lt3  9304  7p3e10  9675  7p6e13  9678  8p3e11  9681  8p5e13  9683  9p3e12  9688  9p4e13  9689  4t3e12  9698  5t3e15  9701  6t3e18  9705  7t3e21  9710  8t3e24  9716  9t3e27  9723  nn01to3  9841  fztpval  10308  fz0to3un2pr  10348  fz0to4untppr  10349  fzo0to42pr  10455  cu2  10890  i3  10893  binom3  10909  fac3  10984  ege2le3  12222  ef4p  12245  cos1bnd  12310  3prm  12690  oddprmge3  12697  dveflem  15440  sincosq3sgn  15542  sincosq4sgn  15543  tangtx  15552  sincos6thpi  15556  binom4  15693  lgsdir2lem3  15749