![]() |
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 12332 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2743 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 (class class class)co 7430 1c1 11153 + caddc 11155 7c7 12323 8c8 12324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-cleq 2726 df-8 12332 |
This theorem is referenced by: 7t4e28 12841 9t9e81 12859 s8len 14938 prmlem2 17153 83prm 17156 163prm 17158 317prm 17159 631prm 17160 2503lem2 17171 2503lem3 17172 4001lem2 17175 4001lem3 17176 4001prm 17178 hgt750lem 34644 hgt750lem2 34645 lcmineqlem 42033 3cubeslem3l 42673 3cubeslem3r 42674 resqrtvalex 43634 imsqrtvalex 43635 fmtno5lem4 47480 fmtno4nprmfac193 47498 m3prm 47516 m7prm 47524 nnsum3primesle9 47718 bgoldbtbndlem1 47729 |
Copyright terms: Public domain | W3C validator |