Theorem 8p1e9 12492

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203  8c8 12403  9c9 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-9 12412

This theorem is used by:  cos2bnd  16356  19prm  17296  139prm  17302  317prm  17304  1259lem2  17310  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  4001lem1  17319  quartlem1  27185  log2ub  27277  hgt750lem2  35281  lcmineqlem  43102  3lexlogpow5ineq2  43105  aks4d1p1  43126  1p8e9  43315  4p5e9  43324  sum9cubes  43683  3cubeslem3l  43696  3cubeslem3r  43697  fmtno5lem3  48639  fmtno5lem4  48640  fmtno4prmfac  48656  fmtno5fac  48666  139prmALT  48680  nfermltl8rev  48839  evengpop3  48895  bgoldbtbndlem1  48902