Definition df-6 12192

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 12184	. 2 class 6
2		c5 12183	. . 3 class 5
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 2 class (5 + 1)
6	1, 5	wceq 1541	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12214  6re  12215  6cn  12216  6pos  12235  6m1e5  12251  5p1e6  12267  3p3e6  12272  4p2e6  12273  5p2e7  12276  5lt6  12301  6p6e12  12662  7p6e13  12666  8p6e14  12672  8p8e16  12674  9p6e15  12679  9p7e16  12680  6t6e36  12696  7t6e42  12701  8t6e48  12707  9t6e54  12714  lt6abl  19807  ppiublem1  27140  ppiublem2  27141  ppiub  27142  bposlem8  27229  lgsdir2lem3  27265  2lgsoddprmlem3d  27351  aks4d1p1p5  42178  rmydioph  43117  expdiophlem2  43125  ceil5half3  47450  stgoldbwt  47886  sbgoldbm  47894