Theorem 8p1e9 12123

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

Syntax hints:   = wceq 1539  (class class class)co 7275  1c1 10872   + caddc 10874  8c8 12034  9c9 12035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-9 12043

This theorem is referenced by:  cos2bnd  15897  19prm  16819  139prm  16825  317prm  16827  1259lem2  16833  1259lem4  16835  1259lem5  16836  1259prm  16837  2503lem1  16838  2503lem2  16839  2503lem3  16840  4001lem1  16842  quartlem1  26007  log2ub  26099  hgt750lem2  32632  lcmineqlem  40060  3lexlogpow5ineq2  40063  aks4d1p1  40084  3cubeslem3l  40508  3cubeslem3r  40509  fmtno5lem3  45007  fmtno5lem4  45008  fmtno4prmfac  45024  fmtno5fac  45034  139prmALT  45048  nfermltl8rev  45194  evengpop3  45250  bgoldbtbndlem1  45257