![]() |
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 11114 | . 2 class 8 | |
2 | c7 11113 | . . 3 class 7 | |
3 | c1 9975 | . . 3 class 1 | |
4 | caddc 9977 | . . 3 class + | |
5 | 2, 3, 4 | co 6690 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1523 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8re 11143 8pos 11159 8m1e7 11180 7p1e8 11195 4p4e8 11202 5p3e8 11204 6p2e8 11207 7p2e9 11210 8nn 11229 7lt8 11253 8p8e16 11656 9p8e17 11664 9p9e18 11665 8t8e64 11700 9t8e72 11707 log2ub 24721 lgsdir2lem1 25095 lgsdir2lem3 25097 rmydioph 37898 |
Copyright terms: Public domain | W3C validator |