Definition df-6 11705

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 11697	. 2 class 6
2		c5 11696	. . 3 class 5
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (5 + 1)
6	1, 5	wceq 1537	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  11727  6re  11728  6cn  11729  6pos  11748  6m1e5  11769  5p1e6  11785  3p3e6  11790  4p2e6  11791  5p2e7  11794  5lt6  11819  6p6e12  12173  7p6e13  12177  8p6e14  12183  8p8e16  12185  9p6e15  12190  9p7e16  12191  6t6e36  12207  7t6e42  12212  8t6e48  12218  9t6e54  12225  lt6abl  19015  ppiublem1  25778  ppiublem2  25779  ppiub  25780  bposlem8  25867  lgsdir2lem3  25903  2lgsoddprmlem3d  25989  rmydioph  39660  expdiophlem2  39668  stgoldbwt  43990  sbgoldbm  43998