![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 7p1e8 | Structured version Visualization version GIF version |
Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
7p1e8 | ⊢ (7 + 1) = 8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 11502 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2781 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 (class class class)co 6970 1c1 10328 + caddc 10330 7c7 11493 8c8 11494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-9 2057 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 df-8 11502 |
This theorem is referenced by: 7t4e28 12017 9t9e81 12035 s8len 14117 prmlem2 16299 83prm 16302 163prm 16304 317prm 16305 631prm 16306 2503lem2 16317 2503lem3 16318 4001lem2 16321 4001lem3 16322 4001prm 16324 hgt750lem 31531 hgt750lem2 31532 fmtno5lem4 43026 fmtno4nprmfac193 43044 m3prm 43062 m7prm 43072 nnsum3primesle9 43267 bgoldbtbndlem1 43278 |
Copyright terms: Public domain | W3C validator |