![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 8p1e9 | Structured version Visualization version GIF version |
Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
8p1e9 | ⊢ (8 + 1) = 9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-9 11729 | . 2 ⊢ 9 = (8 + 1) | |
2 | 1 | eqcomi 2768 | 1 ⊢ (8 + 1) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 (class class class)co 7143 1c1 10561 + caddc 10563 8c8 11720 9c9 11721 |
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 1912 ax-6 1971 ax-7 2016 ax-9 2122 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1783 df-cleq 2751 df-9 11729 |
This theorem is referenced by: cos2bnd 15574 19prm 16494 139prm 16500 317prm 16502 1259lem2 16508 1259lem4 16510 1259lem5 16511 1259prm 16512 2503lem1 16513 2503lem2 16514 2503lem3 16515 4001lem1 16517 quartlem1 25527 log2ub 25619 hgt750lem2 32136 lcmineqlem 39604 3lexlogpow5ineq2 39607 aks4d1p1 39627 3cubeslem3l 39985 3cubeslem3r 39986 fmtno5lem3 44425 fmtno5lem4 44426 fmtno4prmfac 44442 fmtno5fac 44452 139prmALT 44466 nfermltl8rev 44612 evengpop3 44668 bgoldbtbndlem1 44675 |
Copyright terms: Public domain | W3C validator |