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

Theorem 8p1e9 10686
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 10621 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2432 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6244   1c1 9486    + caddc 9488   8c8 10611   9c9 10612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-cleq 2416  df-9 10621
This theorem is referenced by:  cos2bnd  14180  19prm  15027  139prm  15033  317prm  15035  1259lem2  15041  1259lem4  15043  1259lem5  15044  1259prm  15045  2503lem1  15046  2503lem2  15047  2503lem3  15048  4001lem1  15050  quartlem1  23720  log2ub  23812  evengpop3  38706  bgoldbtbndlem1  38713
  Copyright terms: Public domain W3C validator