Theorem 8p1e9 12394

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410  1c1 11105   + caddc 11107  8c8 12305  9c9 12306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-9 12314

This theorem is used by:  cos2bnd  16248  19prm  17182  139prm  17188  317prm  17190  1259lem2  17196  1259lem4  17198  1259lem5  17199  1259prm  17200  2503lem1  17201  2503lem2  17202  2503lem3  17203  4001lem1  17205  quartlem1  27031  log2ub  27123  hgt750lem2  35048  lcmineqlem  42847  3lexlogpow5ineq2  42850  aks4d1p1  42871  sum9cubes  43432  3cubeslem3l  43445  3cubeslem3r  43446  fmtno5lem3  48335  fmtno5lem4  48336  fmtno4prmfac  48352  fmtno5fac  48362  139prmALT  48376  nfermltl8rev  48535  evengpop3  48591  bgoldbtbndlem1  48598