MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  8p1e9 Unicode version

Theorem 8p1e9 10691
Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
8p1e9

Proof of Theorem 8p1e9
StepHypRef Expression
1 df-9 10626 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  8c8 10616  9c9 10617
This theorem is referenced by:  cos2bnd  13923  19prm  14603  139prm  14609  317prm  14611  1259lem2  14614  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  4001lem1  14623  quartlem1  23188  log2ub  23280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-9 10626
  Copyright terms: Public domain W3C validator