Theorem 8p1e9 12390

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103  8c8 12301  9c9 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-9 12310

This theorem is referenced by:  cos2bnd  16244  19prm  17178  139prm  17184  317prm  17186  1259lem2  17192  1259lem4  17194  1259lem5  17195  1259prm  17196  2503lem1  17197  2503lem2  17198  2503lem3  17199  4001lem1  17201  quartlem1  26988  log2ub  27080  hgt750lem2  34984  lcmineqlem  42743  3lexlogpow5ineq2  42746  aks4d1p1  42767  sum9cubes  43330  3cubeslem3l  43343  3cubeslem3r  43344  fmtno5lem3  48230  fmtno5lem4  48231  fmtno4prmfac  48247  fmtno5fac  48257  139prmALT  48271  nfermltl8rev  48430  evengpop3  48486  bgoldbtbndlem1  48493