Definition df-6 12305

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 12297	. 2 class 6
2		c5 12296	. . 3 class 5
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12327  6re  12328  6cn  12329  6pos  12348  6m1e5  12369  5p1e6  12385  3p3e6  12390  4p2e6  12391  5p2e7  12394  5lt6  12419  6p6e12  12780  7p6e13  12784  8p6e14  12790  8p8e16  12792  9p6e15  12797  9p7e16  12798  6t6e36  12814  7t6e42  12819  8t6e48  12825  9t6e54  12832  lt6abl  19874  ppiublem1  27163  ppiublem2  27164  ppiub  27165  bposlem8  27252  lgsdir2lem3  27288  2lgsoddprmlem3d  27374  aks4d1p1p5  42034  rmydioph  42985  expdiophlem2  42993  ceil5half3  47317  stgoldbwt  47738  sbgoldbm  47746