Definition df-6 9370

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 9362	. 2 class 6
2		c5 9361	. . 3 class 5
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 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  9388  6pos  9408  6m1e5  9430  5p1e6  9445  3p3e6  9450  4p2e6  9451  5p2e7  9454  6nn  9475  5lt6  9489  6p6e12  9860  7p6e13  9864  8p6e14  9870  8p8e16  9872  9p6e15  9877  9p7e16  9878  6t6e36  9894  7t6e42  9899  8t6e48  9905  9t6e54  9912  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  bposlem8  16279  lgsdir2lem3  16315  2lgsoddprmlem3d  16395