![]() |
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 12156 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2747 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 (class class class)co 7350 1c1 10986 + caddc 10988 7c7 12147 8c8 12148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2730 df-8 12156 |
This theorem is referenced by: 7t4e28 12663 9t9e81 12681 s8len 14725 prmlem2 16928 83prm 16931 163prm 16933 317prm 16934 631prm 16935 2503lem2 16946 2503lem3 16947 4001lem2 16950 4001lem3 16951 4001prm 16953 hgt750lem 33044 hgt750lem2 33045 lcmineqlem 40440 3cubeslem3l 40911 3cubeslem3r 40912 resqrtvalex 41716 imsqrtvalex 41717 fmtno5lem4 45539 fmtno4nprmfac193 45557 m3prm 45575 m7prm 45583 nnsum3primesle9 45777 bgoldbtbndlem1 45788 |
Copyright terms: Public domain | W3C validator |