Definition df-3 9202

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 9194	. 2 class 3
2		c2 9193	. . 3 class 2
3		c1 8032	. . 3 class 1
4		caddc 8034	. . 3 class +
5	2, 3, 4	co 6017	. 2 class (2 + 1)
6	1, 5	wceq 1397	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9216  3pos  9236  3m1e2  9262  2p2e4  9269  2p1e3  9276  3p3e6  9285  4p3e7  9287  5p3e8  9290  6p3e9  9293  3t3e9  9300  3nn  9305  2lt3  9313  7p3e10  9684  7p6e13  9687  8p3e11  9690  8p5e13  9692  9p3e12  9697  9p4e13  9698  4t3e12  9707  5t3e15  9710  6t3e18  9714  7t3e21  9719  8t3e24  9725  9t3e27  9732  nn01to3  9850  fztpval  10317  fz0to3un2pr  10357  fz0to4untppr  10358  fzo0to42pr  10464  cu2  10899  i3  10902  binom3  10918  fac3  10993  ege2le3  12231  ef4p  12254  cos1bnd  12319  3prm  12699  oddprmge3  12706  dveflem  15449  sincosq3sgn  15551  sincosq4sgn  15552  tangtx  15561  sincos6thpi  15565  binom4  15702  lgsdir2lem3  15758