Definition df-6 12216

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 12208	. 2 class 6
2		c5 12207	. . 3 class 5
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12238  6re  12239  6cn  12240  6pos  12259  6m1e5  12275  5p1e6  12291  3p3e6  12296  4p2e6  12297  5p2e7  12300  5lt6  12325  6p6e12  12685  7p6e13  12689  8p6e14  12695  8p8e16  12697  9p6e15  12702  9p7e16  12703  6t6e36  12719  7t6e42  12724  8t6e48  12730  9t6e54  12737  lt6abl  19828  ppiublem1  27173  ppiublem2  27174  ppiub  27175  bposlem8  27262  lgsdir2lem3  27298  2lgsoddprmlem3d  27384  aks4d1p1p5  42397  rmydioph  43323  expdiophlem2  43331  ceil5half3  47653  stgoldbwt  48089  sbgoldbm  48097