![]() |
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 12272 | . 2 class 8 | |
2 | c7 12271 | . . 3 class 7 | |
3 | c1 11108 | . . 3 class 1 | |
4 | caddc 11110 | . . 3 class + | |
5 | 2, 3, 4 | co 7402 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1533 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 12306 8re 12307 8cn 12308 8pos 12323 8m1e7 12344 7p1e8 12360 4p4e8 12366 5p3e8 12368 6p2e8 12370 7p2e9 12372 7lt8 12403 8p8e16 12762 9p8e17 12769 9p9e18 12770 8t8e64 12797 9t8e72 12804 log2ub 26821 3cubeslem3r 41975 rmydioph 42303 |
Copyright terms: Public domain | W3C validator |