Definition df-6 9367

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 9359	. 2 class 6
2		c5 9358	. . 3 class 5
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class (5 + 1)
6	1, 5	wceq 1402	1 wff 6 = (5 + 1)

This definition is used by:  6re  9385  6pos  9405  6m1e5  9427  5p1e6  9442  3p3e6  9447  4p2e6  9448  5p2e7  9451  6nn  9470  5lt6  9484  6p6e12  9850  7p6e13  9854  8p6e14  9860  8p8e16  9862  9p6e15  9867  9p7e16  9868  6t6e36  9884  7t6e42  9889  8t6e48  9895  9t6e54  9902  lgsdir2lem3  16149  2lgsoddprmlem3d  16229