Definition df-6 12040

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 12032	. 2 class 6
2		c5 12031	. . 3 class 5
3		c1 10872	. . 3 class 1
4		caddc 10874	. . 3 class +
5	2, 3, 4	co 7275	. 2 class (5 + 1)
6	1, 5	wceq 1539	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12062  6re  12063  6cn  12064  6pos  12083  6m1e5  12104  5p1e6  12120  3p3e6  12125  4p2e6  12126  5p2e7  12129  5lt6  12154  6p6e12  12511  7p6e13  12515  8p6e14  12521  8p8e16  12523  9p6e15  12528  9p7e16  12529  6t6e36  12545  7t6e42  12550  8t6e48  12556  9t6e54  12563  lt6abl  19496  ppiublem1  26350  ppiublem2  26351  ppiub  26352  bposlem8  26439  lgsdir2lem3  26475  2lgsoddprmlem3d  26561  aks4d1p1p5  40083  rmydioph  40836  expdiophlem2  40844  stgoldbwt  45228  sbgoldbm  45236