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

Theorem 8p1e9 11035
 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 10963 . 2 9 = (8 + 1)
21eqcomi 2619 1 (8 + 1) = 9
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  8c8 10953  9c9 10954 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-9 10963 This theorem is referenced by:  cos2bnd  14757  19prm  15663  139prm  15669  317prm  15671  1259lem2  15677  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  4001lem1  15686  quartlem1  24384  log2ub  24476  fmtno5lem3  40005  fmtno5lem4  40006  fmtno4prmfac  40022  fmtno5fac  40032  139prmALT  40049  evengpop3  40214  bgoldbtbndlem1  40221
 Copyright terms: Public domain W3C validator