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 11972

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 11964	. 2 class 8
2		c7 11963	. . 3 class 7
3		c1 10803	. . 3 class 1
4		caddc 10805	. . 3 class +
5	2, 3, 4	co 7255	. 2 class (7 + 1)
6	1, 5	wceq 1539	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 11998 8re 11999 8cn 12000 8pos 12015 8m1e7 12036 7p1e8 12052 4p4e8 12058 5p3e8 12060 6p2e8 12062 7p2e9 12064 7lt8 12095 8p8e16 12452 9p8e17 12459 9p9e18 12460 8t8e64 12487 9t8e72 12494 log2ub 26004 3cubeslem3r 40425 rmydioph 40752