Theorem 8p1e9 12053

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

Syntax hints:   = wceq 1539  (class class class)co 7255  1c1 10803   + caddc 10805  8c8 11964  9c9 11965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-9 11973

This theorem is referenced by:  cos2bnd  15825  19prm  16747  139prm  16753  317prm  16755  1259lem2  16761  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem1  16766  2503lem2  16767  2503lem3  16768  4001lem1  16770  quartlem1  25912  log2ub  26004  hgt750lem2  32532  lcmineqlem  39988  3lexlogpow5ineq2  39991  aks4d1p1  40012  3cubeslem3l  40424  3cubeslem3r  40425  fmtno5lem3  44895  fmtno5lem4  44896  fmtno4prmfac  44912  fmtno5fac  44922  139prmALT  44936  nfermltl8rev  45082  evengpop3  45138  bgoldbtbndlem1  45145