![]() |
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 12336 | . 2 ⊢ 9 = (8 + 1) | |
2 | 1 | eqcomi 2735 | 1 ⊢ (8 + 1) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7426 1c1 11161 + caddc 11163 8c8 12327 9c9 12328 |
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-9 12336 |
This theorem is referenced by: cos2bnd 16192 19prm 17122 139prm 17128 317prm 17130 1259lem2 17136 1259lem4 17138 1259lem5 17139 1259prm 17140 2503lem1 17141 2503lem2 17142 2503lem3 17143 4001lem1 17145 quartlem1 26888 log2ub 26980 hgt750lem2 34500 lcmineqlem 41753 3lexlogpow5ineq2 41756 aks4d1p1 41777 sum9cubes 42344 3cubeslem3l 42361 3cubeslem3r 42362 fmtno5lem3 47145 fmtno5lem4 47146 fmtno4prmfac 47162 fmtno5fac 47172 139prmALT 47186 nfermltl8rev 47332 evengpop3 47388 bgoldbtbndlem1 47395 |
Copyright terms: Public domain | W3C validator |