Definition df-6 12325

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 12317	. 2 class 6
2		c5 12316	. . 3 class 5
3		c1 11119	. . 3 class 1
4		caddc 11121	. . 3 class +
5	2, 3, 4	co 7423	. 2 class (5 + 1)
6	1, 5	wceq 1570	1 wff 6 = (5 + 1)

This definition is used by:  6nn  12348  6re  12349  6cn  12350  6m1e5  12389  5p1e6  12405  3p3e6  12410  4p2e6  12411  5p2e7  12414  5lt6  12442  6p6e12  12808  7p6e13  12812  8p6e14  12818  8p8e16  12820  9p6e15  12825  9p7e16  12826  6t6e36  12842  7t6e42  12847  8t6e48  12853  9t6e54  12860  lt6abl  19990  ppiublem1  27396  ppiublem2  27397  ppiub  27398  bposlem8  27485  lgsdir2lem3  27521  2lgsoddprmlem3d  27607  aks4d1p1p5  42875  rmydioph  43774  expdiophlem2  43782  ceil5half3  48116  stgoldbwt  48574  sbgoldbm  48582