Theorem 8p1e9 12505

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   + caddc 11216  8c8 12416  9c9 12417

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-9 12425

This theorem is used by:  cos2bnd  16371  19prm  17311  139prm  17317  317prm  17319  1259lem2  17325  1259lem4  17327  1259lem5  17328  1259prm  17329  2503lem1  17330  2503lem2  17331  2503lem3  17332  4001lem1  17334  quartlem1  27200  log2ub  27292  hgt750lem2  35337  lcmineqlem  43248  3lexlogpow5ineq2  43251  aks4d1p1  43272  1p8e9  43461  4p5e9  43470  sum9cubes  43829  3cubeslem3l  43842  3cubeslem3r  43843  fmtno5lem3  48785  fmtno5lem4  48786  fmtno4prmfac  48802  fmtno5fac  48812  139prmALT  48826  nfermltl8rev  48985  evengpop3  49041  bgoldbtbndlem1  49048