Theorem 8p1e9 12320

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 12245	. 2 ⊢ 9 = (8 + 1)
2	1	eqcomi 2746	1 ⊢ (8 + 1) = 9

Syntax hints:   = wceq 1542  (class class class)co 7361  1c1 11033   + caddc 11035  8c8 12236  9c9 12237

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 2709

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

This theorem is referenced by:  cos2bnd  16149  19prm  17082  139prm  17088  317prm  17090  1259lem2  17096  1259lem4  17098  1259lem5  17099  1259prm  17100  2503lem1  17101  2503lem2  17102  2503lem3  17103  4001lem1  17105  quartlem1  26837  log2ub  26929  hgt750lem2  34815  lcmineqlem  42508  3lexlogpow5ineq2  42511  aks4d1p1  42532  sum9cubes  43122  3cubeslem3l  43135  3cubeslem3r  43136  fmtno5lem3  48033  fmtno5lem4  48034  fmtno4prmfac  48050  fmtno5fac  48060  139prmALT  48074  nfermltl8rev  48233  evengpop3  48289  bgoldbtbndlem1  48296