Definition df-6 12276

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 12268	. 2 class 6
2		c5 12267	. . 3 class 5
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12298  6re  12299  6cn  12300  6pos  12319  6m1e5  12340  5p1e6  12356  3p3e6  12361  4p2e6  12362  5p2e7  12365  5lt6  12390  6p6e12  12748  7p6e13  12752  8p6e14  12758  8p8e16  12760  9p6e15  12765  9p7e16  12766  6t6e36  12782  7t6e42  12787  8t6e48  12793  9t6e54  12800  lt6abl  19758  ppiublem1  26695  ppiublem2  26696  ppiub  26697  bposlem8  26784  lgsdir2lem3  26820  2lgsoddprmlem3d  26906  aks4d1p1p5  40929  rmydioph  41739  expdiophlem2  41747  stgoldbwt  46431  sbgoldbm  46439