Definition df-6 12243

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 12235	. 2 class 6
2		c5 12234	. . 3 class 5
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (5 + 1)
6	1, 5	wceq 1548	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12265  6re  12266  6cn  12267  6pos  12286  6m1e5  12302  5p1e6  12318  3p3e6  12323  4p2e6  12324  5p2e7  12327  5lt6  12352  6p6e12  12713  7p6e13  12717  8p6e14  12723  8p8e16  12725  9p6e15  12730  9p7e16  12731  6t6e36  12747  7t6e42  12752  8t6e48  12758  9t6e54  12765  lt6abl  19864  ppiublem1  27186  ppiublem2  27187  ppiub  27188  bposlem8  27275  lgsdir2lem3  27311  2lgsoddprmlem3d  27397  aks4d1p1p5  42573  rmydioph  43472  expdiophlem2  43480  ceil5half3  47821  stgoldbwt  48279  sbgoldbm  48287