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 12017 | . 2 class 8 | |
2 | c7 12016 | . . 3 class 7 | |
3 | c1 10856 | . . 3 class 1 | |
4 | caddc 10858 | . . 3 class + | |
5 | 2, 3, 4 | co 7268 | . 2 class (7 + 1) |
6 | 1, 5 | wceq 1541 | 1 wff 8 = (7 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 8nn 12051 8re 12052 8cn 12053 8pos 12068 8m1e7 12089 7p1e8 12105 4p4e8 12111 5p3e8 12113 6p2e8 12115 7p2e9 12117 7lt8 12148 8p8e16 12505 9p8e17 12512 9p9e18 12513 8t8e64 12540 9t8e72 12547 log2ub 26080 3cubeslem3r 40489 rmydioph 40816 |
Copyright terms: Public domain | W3C validator |