Definition df-6 12333

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 12325	. 2 class 6
2		c5 12324	. . 3 class 5
3		c1 11156	. . 3 class 1
4		caddc 11158	. . 3 class +
5	2, 3, 4	co 7431	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12355  6re  12356  6cn  12357  6pos  12376  6m1e5  12397  5p1e6  12413  3p3e6  12418  4p2e6  12419  5p2e7  12422  5lt6  12447  6p6e12  12807  7p6e13  12811  8p6e14  12817  8p8e16  12819  9p6e15  12824  9p7e16  12825  6t6e36  12841  7t6e42  12846  8t6e48  12852  9t6e54  12859  lt6abl  19913  ppiublem1  27246  ppiublem2  27247  ppiub  27248  bposlem8  27335  lgsdir2lem3  27371  2lgsoddprmlem3d  27457  aks4d1p1p5  42076  rmydioph  43026  expdiophlem2  43034  ceil5half3  47342  stgoldbwt  47763  sbgoldbm  47771