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 12262

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 12254	. 2 class 8
2		c7 12253	. . 3 class 7
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (7 + 1)
6	1, 5	wceq 1540	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12288 8re 12289 8cn 12290 8pos 12305 8m1e7 12321 7p1e8 12337 4p4e8 12343 5p3e8 12345 6p2e8 12347 7p2e9 12349 7lt8 12380 8p8e16 12742 9p8e17 12749 9p9e18 12750 8t8e64 12777 9t8e72 12784 log2ub 26866 3cubeslem3r 42682 rmydioph 43010