Definition df-3 9096

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 9088	. 2 class 3
2		c2 9087	. . 3 class 2
3		c1 7926	. . 3 class 1
4		caddc 7928	. . 3 class +
5	2, 3, 4	co 5944	. 2 class ( 2 + 1 )
6	1, 5	wceq 1373	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9110  3pos  9130  3m1e2  9156  2p2e4  9163  2p1e3  9170  3p3e6  9179  4p3e7  9181  5p3e8  9184  6p3e9  9187  3t3e9  9194  3nn  9199  2lt3  9207  7p3e10  9578  7p6e13  9581  8p3e11  9584  8p5e13  9586  9p3e12  9591  9p4e13  9592  4t3e12  9601  5t3e15  9604  6t3e18  9608  7t3e21  9613  8t3e24  9619  9t3e27  9626  nn01to3  9738  fztpval  10205  fz0to3un2pr  10245  fz0to4untppr  10246  fzo0to42pr  10349  cu2  10783  i3  10786  binom3  10802  fac3  10877  ege2le3  11982  ef4p  12005  cos1bnd  12070  3prm  12450  oddprmge3  12457  dveflem  15198  sincosq3sgn  15300  sincosq4sgn  15301  tangtx  15310  sincos6thpi  15314  binom4  15451  lgsdir2lem3  15507