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 12435

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 12427	. 2 class 8
2		c7 12426	. . 3 class 7
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (7 + 1)
6	1, 5	wceq 1570	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is used by: 8nn 12462 8re 12463 8cn 12464 8m1e7 12499 7p1e8 12515 4p4e8 12521 5p3e8 12523 6p2e8 12525 7p2e9 12527 7lt8 12561 8p8e16 12929 9p8e17 12936 9p9e18 12937 8t8e64 12964 9t8e72 12971 log2ub 27304 1p8e9 43506 3cubeslem3r 43888 rmydioph 44212