Theorem 8p1e9 12270

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  8c8 12186  9c9 12187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-9 12195

This theorem is referenced by:  cos2bnd  16097  19prm  17029  139prm  17035  317prm  17037  1259lem2  17043  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  4001lem1  17052  quartlem1  26794  log2ub  26886  hgt750lem2  34665  lcmineqlem  42155  3lexlogpow5ineq2  42158  aks4d1p1  42179  sum9cubes  42775  3cubeslem3l  42789  3cubeslem3r  42790  fmtno5lem3  47665  fmtno5lem4  47666  fmtno4prmfac  47682  fmtno5fac  47692  139prmALT  47706  nfermltl8rev  47852  evengpop3  47908  bgoldbtbndlem1  47915