![]() |
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 12324 | . 2 class 8 | |
2 | c7 12323 | . . 3 class 7 | |
3 | c1 11153 | . . 3 class 1 | |
4 | caddc 11155 | . . 3 class + | |
5 | 2, 3, 4 | co 7430 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1536 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 12358 8re 12359 8cn 12360 8pos 12375 8m1e7 12396 7p1e8 12412 4p4e8 12418 5p3e8 12420 6p2e8 12422 7p2e9 12424 7lt8 12455 8p8e16 12816 9p8e17 12823 9p9e18 12824 8t8e64 12851 9t8e72 12858 log2ub 27006 3cubeslem3r 42674 rmydioph 43002 |
Copyright terms: Public domain | W3C validator |