Definition df-6 12306

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 12298	. 2 class 6
2		c5 12297	. . 3 class 5
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (5 + 1)
6	1, 5	wceq 1568	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12329  6re  12330  6cn  12331  6m1e5  12370  5p1e6  12386  3p3e6  12391  4p2e6  12392  5p2e7  12395  5lt6  12423  6p6e12  12789  7p6e13  12793  8p6e14  12799  8p8e16  12801  9p6e15  12806  9p7e16  12807  6t6e36  12823  7t6e42  12828  8t6e48  12834  9t6e54  12841  lt6abl  19964  ppiublem1  27342  ppiublem2  27343  ppiub  27344  bposlem8  27431  lgsdir2lem3  27467  2lgsoddprmlem3d  27553  aks4d1p1p5  42788  rmydioph  43689  expdiophlem2  43697  ceil5half3  48028  stgoldbwt  48486  sbgoldbm  48494