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

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

Proof of Theorem 8p1e9
StepHypRef Expression
1 df-9 9856 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2320 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1633  (class class class)co 5900   1c1 8783    + caddc 8785   8c8 9846   9c9 9847
This theorem is referenced by:  cos2bnd  12515  19prm  13166  139prm  13172  317prm  13174  1259lem2  13177  1259lem4  13179  1259lem5  13180  1259prm  13181  2503lem1  13182  2503lem2  13183  2503lem3  13184  4001lem1  13186  quartlem1  20206  log2ub  20298
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-cleq 2309  df-9 9856
  Copyright terms: Public domain W3C validator