Theorem 8p1e9 12273

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  8c8 12189  9c9 12190

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 12198

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  26765  log2ub  26857  hgt750lem2  34626  lcmineqlem  42035  3lexlogpow5ineq2  42038  aks4d1p1  42059  sum9cubes  42655  3cubeslem3l  42669  3cubeslem3r  42670  fmtno5lem3  47549  fmtno5lem4  47550  fmtno4prmfac  47566  fmtno5fac  47576  139prmALT  47590  nfermltl8rev  47736  evengpop3  47792  bgoldbtbndlem1  47799