Definition df-6 11507

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 11499	. 2 class 6
2		c5 11498	. . 3 class 5
3		c1 10336	. . 3 class 1
4		caddc 10338	. . 3 class +
5	2, 3, 4	co 6976	. 2 class (5 + 1)
6	1, 5	wceq 1507	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  11532  6re  11533  6cn  11534  6pos  11557  6m1e5  11578  5p1e6  11594  3p3e6  11599  4p2e6  11600  5p2e7  11603  5lt6  11628  6p6e12  11987  7p6e13  11991  8p6e14  11997  8p8e16  11999  9p6e15  12004  9p7e16  12005  6t6e36  12021  7t6e42  12026  8t6e48  12032  9t6e54  12039  lt6abl  18769  ppiublem1  25480  ppiublem2  25481  ppiub  25482  bposlem8  25569  lgsdir2lem3  25605  2lgsoddprmlem3d  25691  rmydioph  39013  expdiophlem2  39021  stgoldbwt  43315  sbgoldbm  43323