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 12305

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 12297	. 2 class 8
2		c7 12296	. . 3 class 7
3		c1 11133	. . 3 class 1
4		caddc 11135	. . 3 class +
5	2, 3, 4	co 7414	. 2 class (7 + 1)
6	1, 5	wceq 1534	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12331 8re 12332 8cn 12333 8pos 12348 8m1e7 12369 7p1e8 12385 4p4e8 12391 5p3e8 12393 6p2e8 12395 7p2e9 12397 7lt8 12428 8p8e16 12787 9p8e17 12794 9p9e18 12795 8t8e64 12822 9t8e72 12829 log2ub 26874 3cubeslem3r 42101 rmydioph 42429