Definition df-6 12313

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 12305	. 2 class 6
2		c5 12304	. . 3 class 5
3		c1 11107	. . 3 class 1
4		caddc 11109	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (5 + 1)
6	1, 5	wceq 1569	1 wff 6 = (5 + 1)

This definition is used by:  6nn  12336  6re  12337  6cn  12338  6m1e5  12377  5p1e6  12393  3p3e6  12398  4p2e6  12399  5p2e7  12402  5lt6  12430  6p6e12  12796  7p6e13  12800  8p6e14  12806  8p8e16  12808  9p6e15  12813  9p7e16  12814  6t6e36  12830  7t6e42  12835  8t6e48  12841  9t6e54  12848  lt6abl  19971  ppiublem1  27377  ppiublem2  27378  ppiub  27379  bposlem8  27466  lgsdir2lem3  27502  2lgsoddprmlem3d  27588  aks4d1p1p5  42870  rmydioph  43769  expdiophlem2  43777  ceil5half3  48111  stgoldbwt  48569  sbgoldbm  48577