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 11888 | . 2 class 8 | |
2 | c7 11887 | . . 3 class 7 | |
3 | c1 10727 | . . 3 class 1 | |
4 | caddc 10729 | . . 3 class + | |
5 | 2, 3, 4 | co 7210 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1543 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 11922 8re 11923 8cn 11924 8pos 11939 8m1e7 11960 7p1e8 11976 4p4e8 11982 5p3e8 11984 6p2e8 11986 7p2e9 11988 7lt8 12019 8p8e16 12376 9p8e17 12383 9p9e18 12384 8t8e64 12411 9t8e72 12418 log2ub 25829 3cubeslem3r 40210 rmydioph 40537 |
Copyright terms: Public domain | W3C validator |