Definition df-6 8807

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 8799	. 2 class 6
2		c5 8798	. . 3 class 5
3		c1 7645	. . 3 class 1
4		caddc 7647	. . 3 class +
5	2, 3, 4	co 5782	. 2 class (5 + 1)
6	1, 5	wceq 1332	1 wff 6 = (5 + 1)

This definition is referenced by:  6re  8825  6pos  8845  6m1e5  8867  5p1e6  8881  3p3e6  8886  4p2e6  8887  5p2e7  8890  6nn  8909  5lt6  8923  6p6e12  9279  7p6e13  9283  8p6e14  9289  8p8e16  9291  9p6e15  9296  9p7e16  9297  6t6e36  9313  7t6e42  9318  8t6e48  9324  9t6e54  9331