Definition df-6 10960

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 10951	. 2 class 6
2		c5 10950	. . 3 class 5
3		c1 9816	. . 3 class 1
4		caddc 9818	. . 3 class +
5	2, 3, 4	co 6549	. 2 class (5 + 1)
6	1, 5	wceq 1475	1 wff 6 = (5 + 1)

This definition is referenced by:  6re  10978  6pos  10996  6m1e5  11017  5p1e6  11032  3p3e6  11038  4p2e6  11039  5p2e7  11042  6nn  11066  5lt6  11081  6p6e12  11478  7p6e13  11484  8p6e14  11492  8p8e16  11494  9p6e15  11500  9p7e16  11501  6t6e36  11522  6t6e36OLD  11523  7t6e42  11528  8t6e48  11535  8t6e48OLD  11536  9t6e54  11543  lt6abl  18119  ppiublem1  24727  ppiublem2  24728  ppiub  24729  bposlem8  24816  lgsdir2lem3  24852  2lgsoddprmlem3d  24938  rmydioph  36599  expdiophlem2  36607  stgoldbwt  40198