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 12194

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 12186	. 2 class 8
2		c7 12185	. . 3 class 7
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 2 class (7 + 1)
6	1, 5	wceq 1541	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12220 8re 12221 8cn 12222 8pos 12237 8m1e7 12253 7p1e8 12269 4p4e8 12275 5p3e8 12277 6p2e8 12279 7p2e9 12281 7lt8 12312 8p8e16 12674 9p8e17 12681 9p9e18 12682 8t8e64 12709 9t8e72 12716 log2ub 26886 3cubeslem3r 42790 rmydioph 43117