Theorem 8p1e9 12326

Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
8p1e9	⊢ (8 + 1) = 9

Proof of Theorem 8p1e9

Step	Hyp	Ref	Expression
1		df-9 12251	. 2 ⊢ 9 = (8 + 1)
2	1	eqcomi 2745	1 ⊢ (8 + 1) = 9

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  8c8 12242  9c9 12243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-9 12251

This theorem is referenced by:  cos2bnd  16155  19prm  17088  139prm  17094  317prm  17096  1259lem2  17102  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  quartlem1  26821  log2ub  26913  hgt750lem2  34796  lcmineqlem  42491  3lexlogpow5ineq2  42494  aks4d1p1  42515  sum9cubes  43105  3cubeslem3l  43118  3cubeslem3r  43119  fmtno5lem3  48018  fmtno5lem4  48019  fmtno4prmfac  48035  fmtno5fac  48045  139prmALT  48059  nfermltl8rev  48218  evengpop3  48274  bgoldbtbndlem1  48281