Definition df-6 8985

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 8977	. 2 class 6
2		c5 8976	. . 3 class 5
3		c1 7815	. . 3 class 1
4		caddc 7817	. . 3 class +
5	2, 3, 4	co 5878	. 2 class ( 5 + 1 )
6	1, 5	wceq 1353	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  9003  6pos  9023  6m1e5  9045  5p1e6  9059  3p3e6  9064  4p2e6  9065  5p2e7  9068  6nn  9087  5lt6  9101  6p6e12  9460  7p6e13  9464  8p6e14  9470  8p8e16  9472  9p6e15  9477  9p7e16  9478  6t6e36  9494  7t6e42  9499  8t6e48  9505  9t6e54  9512  lgsdir2lem3  14619  2lgsoddprmlem3d  14646