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 10962 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2619 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 (class class class)co 6549 1c1 9816 + caddc 9818 7c7 10952 8c8 10953 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-8 10962 |
This theorem is referenced by: 7t4e28 11526 9t9e81 11546 s8len 13498 prmlem2 15665 83prm 15668 163prm 15670 317prm 15671 631prm 15672 2503lem2 15683 2503lem3 15684 4001lem2 15687 4001lem3 15688 4001prm 15690 fmtno5lem4 40006 fmtno4nprmfac193 40024 m3prm 40044 m7prm 40054 nnsum3primesle9 40210 bgoldbtbndlem1 40221 |
Copyright terms: Public domain | W3C validator |