Definition df-6 12284

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 12276	. 2 class 6
2		c5 12275	. . 3 class 5
3		c1 11115	. . 3 class 1
4		caddc 11117	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12306  6re  12307  6cn  12308  6pos  12327  6m1e5  12348  5p1e6  12364  3p3e6  12369  4p2e6  12370  5p2e7  12373  5lt6  12398  6p6e12  12756  7p6e13  12760  8p6e14  12766  8p8e16  12768  9p6e15  12773  9p7e16  12774  6t6e36  12790  7t6e42  12795  8t6e48  12801  9t6e54  12808  lt6abl  19805  ppiublem1  26942  ppiublem2  26943  ppiub  26944  bposlem8  27031  lgsdir2lem3  27067  2lgsoddprmlem3d  27153  aks4d1p1p5  41247  rmydioph  42056  expdiophlem2  42064  stgoldbwt  46743  sbgoldbm  46751