Definition df-6 9169

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 9161	. 2 class 6
2		c5 9160	. . 3 class 5
3		c1 7996	. . 3 class 1
4		caddc 7998	. . 3 class +
5	2, 3, 4	co 6000	. 2 class (5 + 1)
6	1, 5	wceq 1395	1 wff 6 = (5 + 1)

This definition is referenced by:  6re  9187  6pos  9207  6m1e5  9229  5p1e6  9244  3p3e6  9249  4p2e6  9250  5p2e7  9253  6nn  9272  5lt6  9286  6p6e12  9647  7p6e13  9651  8p6e14  9657  8p8e16  9659  9p6e15  9664  9p7e16  9665  6t6e36  9681  7t6e42  9686  8t6e48  9692  9t6e54  9699  lgsdir2lem3  15703  2lgsoddprmlem3d  15783