Definition df-6 12229

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 12221	. 2 class 6
2		c5 12220	. . 3 class 5
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12251  6re  12252  6cn  12253  6pos  12272  6m1e5  12288  5p1e6  12304  3p3e6  12309  4p2e6  12310  5p2e7  12313  5lt6  12338  6p6e12  12699  7p6e13  12703  8p6e14  12709  8p8e16  12711  9p6e15  12716  9p7e16  12717  6t6e36  12733  7t6e42  12738  8t6e48  12744  9t6e54  12751  lt6abl  19809  ppiublem1  27146  ppiublem2  27147  ppiub  27148  bposlem8  27235  lgsdir2lem3  27271  2lgsoddprmlem3d  27357  aks4d1p1p5  42056  rmydioph  42996  expdiophlem2  43004  ceil5half3  47334  stgoldbwt  47770  sbgoldbm  47778