Definition df-6 9376

Description: Define the number 6. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-6	|- 6 = ( 5 + 1 )

Detailed syntax breakdown of Definition df-6

Step	Hyp	Ref	Expression
1		c6 9368	. 2 class 6
2		c5 9367	. . 3 class 5
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 5 + 1 )
6	1, 5	wceq 1402	1 wff 6 = ( 5 + 1 )

This definition is used by:  6re  9394  6pos  9414  6m1e5  9436  5p1e6  9451  3p3e6  9456  4p2e6  9457  5p2e7  9460  6nn  9481  5lt6  9495  6p6e12  9866  7p6e13  9870  8p6e14  9876  8p8e16  9878  9p6e15  9883  9p7e16  9884  6t6e36  9900  7t6e42  9905  8t6e48  9911  9t6e54  9918  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  bposlem8  16318  lgsdir2lem3  16354  2lgsoddprmlem3d  16434