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 12308

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 12300	. 2 class 8
2		c7 12299	. . 3 class 7
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (7 + 1)
6	1, 5	wceq 1568	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12335 8re 12336 8cn 12337 8m1e7 12372 7p1e8 12388 4p4e8 12394 5p3e8 12396 6p2e8 12398 7p2e9 12400 7lt8 12434 8p8e16 12801 9p8e17 12808 9p9e18 12809 8t8e64 12836 9t8e72 12843 log2ub 27090 3cubeslem3r 43366 rmydioph 43689