Definition df-6 9134

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 9126	. 2 class 6
2		c5 9125	. . 3 class 5
3		c1 7961	. . 3 class 1
4		caddc 7963	. . 3 class +
5	2, 3, 4	co 5967	. 2 class ( 5 + 1 )
6	1, 5	wceq 1373	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  9152  6pos  9172  6m1e5  9194  5p1e6  9209  3p3e6  9214  4p2e6  9215  5p2e7  9218  6nn  9237  5lt6  9251  6p6e12  9612  7p6e13  9616  8p6e14  9622  8p8e16  9624  9p6e15  9629  9p7e16  9630  6t6e36  9646  7t6e42  9651  8t6e48  9657  9t6e54  9664  lgsdir2lem3  15622  2lgsoddprmlem3d  15702