Theorem 8p1e9 12261

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

Syntax hints:   = wceq 1540  (class class class)co 7340  1c1 10998   + caddc 11000  8c8 12177  9c9 12178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-9 12186

This theorem is referenced by:  cos2bnd  16084  19prm  17016  139prm  17022  317prm  17024  1259lem2  17030  1259lem4  17032  1259lem5  17033  1259prm  17034  2503lem1  17035  2503lem2  17036  2503lem3  17037  4001lem1  17039  quartlem1  26748  log2ub  26840  hgt750lem2  34633  lcmineqlem  42042  3lexlogpow5ineq2  42045  aks4d1p1  42066  sum9cubes  42662  3cubeslem3l  42676  3cubeslem3r  42677  fmtno5lem3  47553  fmtno5lem4  47554  fmtno4prmfac  47570  fmtno5fac  47580  139prmALT  47594  nfermltl8rev  47740  evengpop3  47796  bgoldbtbndlem1  47803