Definition df-6 12279

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 12271	. 2 class 6
2		c5 12270	. . 3 class 5
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7409	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12301  6re  12302  6cn  12303  6pos  12322  6m1e5  12343  5p1e6  12359  3p3e6  12364  4p2e6  12365  5p2e7  12368  5lt6  12393  6p6e12  12751  7p6e13  12755  8p6e14  12761  8p8e16  12763  9p6e15  12768  9p7e16  12769  6t6e36  12785  7t6e42  12790  8t6e48  12796  9t6e54  12803  lt6abl  19763  ppiublem1  26705  ppiublem2  26706  ppiub  26707  bposlem8  26794  lgsdir2lem3  26830  2lgsoddprmlem3d  26916  aks4d1p1p5  40940  rmydioph  41753  expdiophlem2  41761  stgoldbwt  46444  sbgoldbm  46452