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 12362

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 12354	. 2 class 8
2		c7 12353	. . 3 class 7
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (7 + 1)
6	1, 5	wceq 1537	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12388 8re 12389 8cn 12390 8pos 12405 8m1e7 12426 7p1e8 12442 4p4e8 12448 5p3e8 12450 6p2e8 12452 7p2e9 12454 7lt8 12485 8p8e16 12844 9p8e17 12851 9p9e18 12852 8t8e64 12879 9t8e72 12886 log2ub 27010 3cubeslem3r 42643 rmydioph 42971