Definition df-6 9302

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 9294	. 2 class 6
2		c5 9293	. . 3 class 5
3		c1 8130	. . 3 class 1
4		caddc 8132	. . 3 class +
5	2, 3, 4	co 6052	. 2 class ( 5 + 1 )
6	1, 5	wceq 1398	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  9320  6pos  9340  6m1e5  9362  5p1e6  9377  3p3e6  9382  4p2e6  9383  5p2e7  9386  6nn  9405  5lt6  9419  6p6e12  9785  7p6e13  9789  8p6e14  9795  8p8e16  9797  9p6e15  9802  9p7e16  9803  6t6e36  9819  7t6e42  9824  8t6e48  9830  9t6e54  9837  lgsdir2lem3  15920  2lgsoddprmlem3d  16000