Definition df-6 12334

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 12326	. 2 class 6
2		c5 12325	. . 3 class 5
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (5 + 1)
6	1, 5	wceq 1570	1 wff 6 = (5 + 1)

This definition is used by:  6nn  12357  6re  12358  6cn  12359  6m1e5  12398  5p1e6  12414  3p3e6  12419  4p2e6  12420  5p2e7  12423  5lt6  12451  6p6e12  12818  7p6e13  12822  8p6e14  12828  8p8e16  12830  9p6e15  12835  9p7e16  12836  6t6e36  12852  7t6e42  12857  8t6e48  12863  9t6e54  12870  lt6abl  20023  ppiublem1  27436  ppiublem2  27437  ppiub  27438  bposlem8  27525  lgsdir2lem3  27561  2lgsoddprmlem3d  27647  aks4d1p1p5  42928  1p6e7  43116  rmydioph  43842  expdiophlem2  43850  ceil5half3  48221  stgoldbwt  48679  sbgoldbm  48687