Definition df-6 12212

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 12204	. 2 class 6
2		c5 12203	. . 3 class 5
3		c1 11027	. . 3 class 1
4		caddc 11029	. . 3 class +
5	2, 3, 4	co 7358	. 2 class (5 + 1)
6	1, 5	wceq 1541	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12234  6re  12235  6cn  12236  6pos  12255  6m1e5  12271  5p1e6  12287  3p3e6  12292  4p2e6  12293  5p2e7  12296  5lt6  12321  6p6e12  12681  7p6e13  12685  8p6e14  12691  8p8e16  12693  9p6e15  12698  9p7e16  12699  6t6e36  12715  7t6e42  12720  8t6e48  12726  9t6e54  12733  lt6abl  19824  ppiublem1  27169  ppiublem2  27170  ppiub  27171  bposlem8  27258  lgsdir2lem3  27294  2lgsoddprmlem3d  27380  aks4d1p1p5  42329  rmydioph  43256  expdiophlem2  43264  ceil5half3  47586  stgoldbwt  48022  sbgoldbm  48030