Definition df-6 12038

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 12030	. 2 class 6
2		c5 12029	. . 3 class 5
3		c1 10871	. . 3 class 1
4		caddc 10873	. . 3 class +
5	2, 3, 4	co 7269	. 2 class (5 + 1)
6	1, 5	wceq 1542	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12060  6re  12061  6cn  12062  6pos  12081  6m1e5  12102  5p1e6  12118  3p3e6  12123  4p2e6  12124  5p2e7  12127  5lt6  12152  6p6e12  12508  7p6e13  12512  8p6e14  12518  8p8e16  12520  9p6e15  12525  9p7e16  12526  6t6e36  12542  7t6e42  12547  8t6e48  12553  9t6e54  12560  lt6abl  19492  ppiublem1  26346  ppiublem2  26347  ppiub  26348  bposlem8  26435  lgsdir2lem3  26471  2lgsoddprmlem3d  26557  aks4d1p1p5  40078  rmydioph  40831  expdiophlem2  40839  stgoldbwt  45195  sbgoldbm  45203