Definition df-3 9170

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 9162	. 2 class 3
2		c2 9161	. . 3 class 2
3		c1 8000	. . 3 class 1
4		caddc 8002	. . 3 class +
5	2, 3, 4	co 6001	. 2 class ( 2 + 1 )
6	1, 5	wceq 1395	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9184  3pos  9204  3m1e2  9230  2p2e4  9237  2p1e3  9244  3p3e6  9253  4p3e7  9255  5p3e8  9258  6p3e9  9261  3t3e9  9268  3nn  9273  2lt3  9281  7p3e10  9652  7p6e13  9655  8p3e11  9658  8p5e13  9660  9p3e12  9665  9p4e13  9666  4t3e12  9675  5t3e15  9678  6t3e18  9682  7t3e21  9687  8t3e24  9693  9t3e27  9700  nn01to3  9812  fztpval  10279  fz0to3un2pr  10319  fz0to4untppr  10320  fzo0to42pr  10426  cu2  10860  i3  10863  binom3  10879  fac3  10954  ege2le3  12182  ef4p  12205  cos1bnd  12270  3prm  12650  oddprmge3  12657  dveflem  15400  sincosq3sgn  15502  sincosq4sgn  15503  tangtx  15512  sincos6thpi  15516  binom4  15653  lgsdir2lem3  15709