Definition df-6 12253

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 12245	. 2 class 6
2		c5 12244	. . 3 class 5
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12275  6re  12276  6cn  12277  6pos  12296  6m1e5  12312  5p1e6  12328  3p3e6  12333  4p2e6  12334  5p2e7  12337  5lt6  12362  6p6e12  12723  7p6e13  12727  8p6e14  12733  8p8e16  12735  9p6e15  12740  9p7e16  12741  6t6e36  12757  7t6e42  12762  8t6e48  12768  9t6e54  12775  lt6abl  19825  ppiublem1  27113  ppiublem2  27114  ppiub  27115  bposlem8  27202  lgsdir2lem3  27238  2lgsoddprmlem3d  27324  aks4d1p1p5  42063  rmydioph  43003  expdiophlem2  43011  ceil5half3  47341  stgoldbwt  47777  sbgoldbm  47785