Definition df-6 9349

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 9341	. 2 class 6
2		c5 9340	. . 3 class 5
3		c1 8173	. . 3 class 1
4		caddc 8175	. . 3 class +
5	2, 3, 4	co 6078	. 2 class ( 5 + 1 )
6	1, 5	wceq 1402	1 wff 6 = ( 5 + 1 )

This definition is referenced by:  6re  9367  6pos  9387  6m1e5  9409  5p1e6  9424  3p3e6  9429  4p2e6  9430  5p2e7  9433  6nn  9452  5lt6  9466  6p6e12  9832  7p6e13  9836  8p6e14  9842  8p8e16  9844  9p6e15  9849  9p7e16  9850  6t6e36  9866  7t6e42  9871  8t6e48  9877  9t6e54  9884  lgsdir2lem3  16066  2lgsoddprmlem3d  16146