Definition df-6 12260

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 12252	. 2 class 6
2		c5 12251	. . 3 class 5
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12282  6re  12283  6cn  12284  6pos  12303  6m1e5  12319  5p1e6  12335  3p3e6  12340  4p2e6  12341  5p2e7  12344  5lt6  12369  6p6e12  12730  7p6e13  12734  8p6e14  12740  8p8e16  12742  9p6e15  12747  9p7e16  12748  6t6e36  12764  7t6e42  12769  8t6e48  12775  9t6e54  12782  lt6abl  19832  ppiublem1  27120  ppiublem2  27121  ppiub  27122  bposlem8  27209  lgsdir2lem3  27245  2lgsoddprmlem3d  27331  aks4d1p1p5  42070  rmydioph  43010  expdiophlem2  43018  ceil5half3  47345  stgoldbwt  47781  sbgoldbm  47789