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 11085 | . 2 ⊢ 8 = (7 + 1) | |
2 | 1 | eqcomi 2631 | 1 ⊢ (7 + 1) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 (class class class)co 6650 1c1 9937 + caddc 9939 7c7 11075 8c8 11076 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-8 11085 |
This theorem is referenced by: 7t4e28 11650 9t9e81 11670 s8len 13648 prmlem2 15827 83prm 15830 163prm 15832 317prm 15833 631prm 15834 2503lem2 15845 2503lem3 15846 4001lem2 15849 4001lem3 15850 4001prm 15852 hgt750lem 30729 hgt750lem2 30730 fmtno5lem4 41468 fmtno4nprmfac193 41486 m3prm 41506 m7prm 41516 nnsum3primesle9 41682 bgoldbtbndlem1 41693 |
Copyright terms: Public domain | W3C validator |