Definition df-6 9070

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 9062	. 2 class 6
2		c5 9061	. . 3 class 5
3		c1 7897	. . 3 class 1
4		caddc 7899	. . 3 class +
5	2, 3, 4	co 5925	. 2 class ( 5 + 1 )
6	1, 5	wceq 1364	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  9088  6pos  9108  6m1e5  9130  5p1e6  9145  3p3e6  9150  4p2e6  9151  5p2e7  9154  6nn  9173  5lt6  9187  6p6e12  9547  7p6e13  9551  8p6e14  9557  8p8e16  9559  9p6e15  9564  9p7e16  9565  6t6e36  9581  7t6e42  9586  8t6e48  9592  9t6e54  9599  lgsdir2lem3  15355  2lgsoddprmlem3d  15435