df-8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-8		Structured version Visualization version GIF version

Definition df-8 12239

Description: Define the number 8. (Contributed by NM, 27-May-1999.)

**Assertion**
Ref	Expression
df-8	⊢ 8 = (7 + 1)

**Detailed syntax breakdown of Definition df-8**
Step	Hyp	Ref	Expression
1		c8 12231	. 2 class 8
2		c7 12230	. . 3 class 7
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (7 + 1)
6	1, 5	wceq 1542	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12265 8re 12266 8cn 12267 8pos 12282 8m1e7 12298 7p1e8 12314 4p4e8 12320 5p3e8 12322 6p2e8 12324 7p2e9 12326 7lt8 12357 8p8e16 12719 9p8e17 12726 9p9e18 12727 8t8e64 12754 9t8e72 12761 log2ub 26901 3cubeslem3r 43107 rmydioph 43430