![]() |
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 11292 | . 2 ⊢ 9 = (8 + 1) | |
2 | 1 | eqcomi 2780 | 1 ⊢ (8 + 1) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 (class class class)co 6796 1c1 10143 + caddc 10145 8c8 11282 9c9 11283 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-cleq 2764 df-9 11292 |
This theorem is referenced by: cos2bnd 15124 19prm 16032 139prm 16038 317prm 16040 1259lem2 16046 1259lem4 16048 1259lem5 16049 1259prm 16050 2503lem1 16051 2503lem2 16052 2503lem3 16053 4001lem1 16055 quartlem1 24805 log2ub 24897 hgt750lem2 31070 fmtno5lem3 41990 fmtno5lem4 41991 fmtno4prmfac 42007 fmtno5fac 42017 139prmALT 42034 evengpop3 42209 bgoldbtbndlem1 42216 |
Copyright terms: Public domain | W3C validator |