Definition df-6 9369

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 9361	. 2 class 6
2		c5 9360	. . 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  9387  6pos  9407  6m1e5  9429  5p1e6  9444  3p3e6  9449  4p2e6  9450  5p2e7  9453  6nn  9474  5lt6  9488  6p6e12  9859  7p6e13  9863  8p6e14  9869  8p8e16  9871  9p6e15  9876  9p7e16  9877  6t6e36  9893  7t6e42  9898  8t6e48  9904  9t6e54  9911  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  lgsdir2lem3  16247  2lgsoddprmlem3d  16327