Definition df-6 11945

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 11937	. 2 class 6
2		c5 11936	. . 3 class 5
3		c1 10778	. . 3 class 1
4		caddc 10780	. . 3 class +
5	2, 3, 4	co 7252	. 2 class (5 + 1)
6	1, 5	wceq 1543	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  11967  6re  11968  6cn  11969  6pos  11988  6m1e5  12009  5p1e6  12025  3p3e6  12030  4p2e6  12031  5p2e7  12034  5lt6  12059  6p6e12  12415  7p6e13  12419  8p6e14  12425  8p8e16  12427  9p6e15  12432  9p7e16  12433  6t6e36  12449  7t6e42  12454  8t6e48  12460  9t6e54  12467  lt6abl  19386  ppiublem1  26230  ppiublem2  26231  ppiub  26232  bposlem8  26319  lgsdir2lem3  26355  2lgsoddprmlem3d  26441  aks4d1p1p5  39989  rmydioph  40724  expdiophlem2  40732  stgoldbwt  45089  sbgoldbm  45097