Definition df-6 12360

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 12352	. 2 class 6
2		c5 12351	. . 3 class 5
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (5 + 1)
6	1, 5	wceq 1537	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12382  6re  12383  6cn  12384  6pos  12403  6m1e5  12424  5p1e6  12440  3p3e6  12445  4p2e6  12446  5p2e7  12449  5lt6  12474  6p6e12  12832  7p6e13  12836  8p6e14  12842  8p8e16  12844  9p6e15  12849  9p7e16  12850  6t6e36  12866  7t6e42  12871  8t6e48  12877  9t6e54  12884  lt6abl  19937  ppiublem1  27264  ppiublem2  27265  ppiub  27266  bposlem8  27353  lgsdir2lem3  27389  2lgsoddprmlem3d  27475  aks4d1p1p5  42032  rmydioph  42971  expdiophlem2  42979  stgoldbwt  47650  sbgoldbm  47658