Definition df-6 12226

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 12218	. 2 class 6
2		c5 12217	. . 3 class 5
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12248  6re  12249  6cn  12250  6pos  12269  6m1e5  12285  5p1e6  12301  3p3e6  12306  4p2e6  12307  5p2e7  12310  5lt6  12335  6p6e12  12695  7p6e13  12699  8p6e14  12705  8p8e16  12707  9p6e15  12712  9p7e16  12713  6t6e36  12729  7t6e42  12734  8t6e48  12740  9t6e54  12747  lt6abl  19841  ppiublem1  27186  ppiublem2  27187  ppiub  27188  bposlem8  27275  lgsdir2lem3  27311  2lgsoddprmlem3d  27397  aks4d1p1p5  42474  rmydioph  43400  expdiophlem2  43408  ceil5half3  47729  stgoldbwt  48165  sbgoldbm  48173