Definition df-6 12210

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 12202	. 2 class 6
2		c5 12201	. . 3 class 5
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (5 + 1)
6	1, 5	wceq 1541	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12232  6re  12233  6cn  12234  6pos  12253  6m1e5  12269  5p1e6  12285  3p3e6  12290  4p2e6  12291  5p2e7  12294  5lt6  12319  6p6e12  12679  7p6e13  12683  8p6e14  12689  8p8e16  12691  9p6e15  12696  9p7e16  12697  6t6e36  12713  7t6e42  12718  8t6e48  12724  9t6e54  12731  lt6abl  19822  ppiublem1  27167  ppiublem2  27168  ppiub  27169  bposlem8  27256  lgsdir2lem3  27292  2lgsoddprmlem3d  27378  aks4d1p1p5  42268  rmydioph  43198  expdiophlem2  43206  ceil5half3  47528  stgoldbwt  47964  sbgoldbm  47972