Definition df-6 12237

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 12229	. 2 class 6
2		c5 12228	. . 3 class 5
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12259  6re  12260  6cn  12261  6pos  12280  6m1e5  12296  5p1e6  12312  3p3e6  12317  4p2e6  12318  5p2e7  12321  5lt6  12346  6p6e12  12707  7p6e13  12711  8p6e14  12717  8p8e16  12719  9p6e15  12724  9p7e16  12725  6t6e36  12741  7t6e42  12746  8t6e48  12752  9t6e54  12759  lt6abl  19859  ppiublem1  27153  ppiublem2  27154  ppiub  27155  bposlem8  27242  lgsdir2lem3  27278  2lgsoddprmlem3d  27364  aks4d1p1p5  42502  rmydioph  43430  expdiophlem2  43438  ceil5half3  47782  stgoldbwt  48240  sbgoldbm  48248