Definition df-6 12286

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 12278	. 2 class 6
2		c5 12277	. . 3 class 5
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (5 + 1)
6	1, 5	wceq 1562	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12309  6re  12310  6cn  12311  6m1e5  12350  5p1e6  12366  3p3e6  12371  4p2e6  12372  5p2e7  12375  5lt6  12403  6p6e12  12769  7p6e13  12773  8p6e14  12779  8p8e16  12781  9p6e15  12786  9p7e16  12787  6t6e36  12803  7t6e42  12808  8t6e48  12814  9t6e54  12821  lt6abl  19937  ppiublem1  27268  ppiublem2  27269  ppiub  27270  bposlem8  27357  lgsdir2lem3  27393  2lgsoddprmlem3d  27479  aks4d1p1p5  42697  rmydioph  43596  expdiophlem2  43604  ceil5half3  47945  stgoldbwt  48403  sbgoldbm  48411