![]() |
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 11498 | . 2 class 8 | |
2 | c7 11497 | . . 3 class 7 | |
3 | c1 10332 | . . 3 class 1 | |
4 | caddc 10334 | . . 3 class + | |
5 | 2, 3, 4 | co 6974 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1507 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 11537 8re 11538 8cn 11539 8pos 11556 8m1e7 11577 7p1e8 11593 4p4e8 11599 5p3e8 11601 6p2e8 11603 7p2e9 11605 7lt8 11636 8p8e16 11996 9p8e17 12003 9p9e18 12004 8t8e64 12031 9t8e72 12038 log2ub 25223 rmydioph 38985 |
Copyright terms: Public domain | W3C validator |