Definition df-3 9206

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 9198	. 2 class 3
2		c2 9197	. . 3 class 2
3		c1 8036	. . 3 class 1
4		caddc 8038	. . 3 class +
5	2, 3, 4	co 6021	. 2 class ( 2 + 1 )
6	1, 5	wceq 1397	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  9220  3pos  9240  3m1e2  9266  2p2e4  9273  2p1e3  9280  3p3e6  9289  4p3e7  9291  5p3e8  9294  6p3e9  9297  3t3e9  9304  3nn  9309  2lt3  9317  7p3e10  9688  7p6e13  9691  8p3e11  9694  8p5e13  9696  9p3e12  9701  9p4e13  9702  4t3e12  9711  5t3e15  9714  6t3e18  9718  7t3e21  9723  8t3e24  9729  9t3e27  9736  nn01to3  9854  fztpval  10321  fz0to3un2pr  10361  fz0to4untppr  10362  fzo0to42pr  10469  cu2  10904  i3  10907  binom3  10923  fac3  10998  ege2le3  12253  ef4p  12276  cos1bnd  12341  3prm  12721  oddprmge3  12728  dveflem  15477  sincosq3sgn  15579  sincosq4sgn  15580  tangtx  15589  sincos6thpi  15593  binom4  15730  lgsdir2lem3  15786  konigsberglem5  16370