Definition df-6 8102

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 8093	. 2 class 6
2		c5 8092	. . 3 class 5
3		c1 6982	. . 3 class 1
4		caddc 6984	. . 3 class +
5	2, 3, 4	co 5532	. 2 class ( 5 + 1 )
6	1, 5	wceq 1284	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  8120  6pos  8140  5p1e6  8169  3p3e6  8174  4p2e6  8175  5p2e7  8178  6nn  8197  5lt6  8211  6p6e12  8550  7p6e13  8554  8p6e14  8560  8p8e16  8562  9p6e15  8567  9p7e16  8568  6t6e36  8584  7t6e42  8589  8t6e48  8595  9t6e54  8602