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 10953 | . 2 class 8 | |
2 | c7 10952 | . . 3 class 7 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1475 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8re 10982 8pos 10998 8m1e7 11019 7p1e8 11034 4p4e8 11041 5p3e8 11043 6p2e8 11046 7p2e9 11049 8nn 11068 7lt8 11092 8p8e16 11494 9p8e17 11502 9p9e18 11503 8t8e64 11538 9t8e72 11545 log2ub 24476 lgsdir2lem1 24850 lgsdir2lem3 24852 rmydioph 36599 |
Copyright terms: Public domain | W3C validator |