Theorem 7p1e8 11157

Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
7p1e8	|- ( 7 + 1 ) = 8

Proof of Theorem 7p1e8

Step	Hyp	Ref	Expression
1		df-8 11085	. 2 |- 8 = ( 7 + 1 )
2	1	eqcomi 2631	1 |- ( 7 + 1 ) = 8

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   7c7 11075   8c8 11076

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-8 11085

This theorem is referenced by:  7t4e28  11650  9t9e81  11670  s8len  13648  prmlem2  15827  83prm  15830  163prm  15832  317prm  15833  631prm  15834  2503lem2  15845  2503lem3  15846  4001lem2  15849  4001lem3  15850  4001prm  15852  hgt750lem  30729  hgt750lem2  30730  fmtno5lem4  41468  fmtno4nprmfac193  41486  m3prm  41506  m7prm  41516  nnsum3primesle9  41682  bgoldbtbndlem1  41693