Theorem 8p1e9 11158

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 11086	. 2 |- 9 = ( 8 + 1 )
2	1	eqcomi 2631	1 |- ( 8 + 1 ) = 9

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   8c8 11076   9c9 11077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-9 11086

This theorem is referenced by:  cos2bnd  14918  19prm  15825  139prm  15831  317prm  15833  1259lem2  15839  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  4001lem1  15848  quartlem1  24584  log2ub  24676  hgt750lem2  30730  fmtno5lem3  41467  fmtno5lem4  41468  fmtno4prmfac  41484  fmtno5fac  41494  139prmALT  41511  evengpop3  41686  bgoldbtbndlem1  41693