Definition df-6 12245

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 12237	. 2 class 6
2		c5 12236	. . 3 class 5
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12267  6re  12268  6cn  12269  6pos  12288  6m1e5  12304  5p1e6  12320  3p3e6  12325  4p2e6  12326  5p2e7  12329  5lt6  12354  6p6e12  12715  7p6e13  12719  8p6e14  12725  8p8e16  12727  9p6e15  12732  9p7e16  12733  6t6e36  12749  7t6e42  12754  8t6e48  12760  9t6e54  12767  lt6abl  19867  ppiublem1  27162  ppiublem2  27163  ppiub  27164  bposlem8  27251  lgsdir2lem3  27287  2lgsoddprmlem3d  27373  aks4d1p1p5  42511  rmydioph  43439  expdiophlem2  43447  ceil5half3  47785  stgoldbwt  48243  sbgoldbm  48251