![]() |
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 12327 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2735 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7416 1c1 11150 + caddc 11152 7c7 12318 8c8 12319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-8 12327 |
This theorem is referenced by: 7t4e28 12834 9t9e81 12852 s8len 14907 prmlem2 17117 83prm 17120 163prm 17122 317prm 17123 631prm 17124 2503lem2 17135 2503lem3 17136 4001lem2 17139 4001lem3 17140 4001prm 17142 hgt750lem 34510 hgt750lem2 34511 lcmineqlem 41764 3cubeslem3l 42380 3cubeslem3r 42381 resqrtvalex 43349 imsqrtvalex 43350 fmtno5lem4 47164 fmtno4nprmfac193 47182 m3prm 47200 m7prm 47208 nnsum3primesle9 47402 bgoldbtbndlem1 47413 |
Copyright terms: Public domain | W3C validator |