Definition df-3 9131

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 9123	. 2 class 3
2		c2 9122	. . 3 class 2
3		c1 7961	. . 3 class 1
4		caddc 7963	. . 3 class +
5	2, 3, 4	co 5967	. 2 class ( 2 + 1 )
6	1, 5	wceq 1373	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9145  3pos  9165  3m1e2  9191  2p2e4  9198  2p1e3  9205  3p3e6  9214  4p3e7  9216  5p3e8  9219  6p3e9  9222  3t3e9  9229  3nn  9234  2lt3  9242  7p3e10  9613  7p6e13  9616  8p3e11  9619  8p5e13  9621  9p3e12  9626  9p4e13  9627  4t3e12  9636  5t3e15  9639  6t3e18  9643  7t3e21  9648  8t3e24  9654  9t3e27  9661  nn01to3  9773  fztpval  10240  fz0to3un2pr  10280  fz0to4untppr  10281  fzo0to42pr  10386  cu2  10820  i3  10823  binom3  10839  fac3  10914  ege2le3  12097  ef4p  12120  cos1bnd  12185  3prm  12565  oddprmge3  12572  dveflem  15313  sincosq3sgn  15415  sincosq4sgn  15416  tangtx  15425  sincos6thpi  15429  binom4  15566  lgsdir2lem3  15622