Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-8 | Structured version Visualization version GIF version |
Description: Define the number 8. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-8 | ⊢ 8 = (7 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c8 11687 | . 2 class 8 | |
2 | c7 11686 | . . 3 class 7 | |
3 | c1 10527 | . . 3 class 1 | |
4 | caddc 10529 | . . 3 class + | |
5 | 2, 3, 4 | co 7145 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1528 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 11721 8re 11722 8cn 11723 8pos 11738 8m1e7 11759 7p1e8 11775 4p4e8 11781 5p3e8 11783 6p2e8 11785 7p2e9 11787 7lt8 11818 8p8e16 12173 9p8e17 12180 9p9e18 12181 8t8e64 12208 9t8e72 12215 log2ub 25455 3cubeslem3r 39164 rmydioph 39491 |
Copyright terms: Public domain | W3C validator |