Theorem 7p1e8 11789

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 11709	. 2 ⊢ 8 = (7 + 1)
2	1	eqcomi 2832	1 ⊢ (7 + 1) = 8

Syntax hints:   = wceq 1537  (class class class)co 7158  1c1 10540   + caddc 10542  7c7 11700  8c8 11701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-8 11709

This theorem is referenced by:  7t4e28  12212  9t9e81  12230  s8len  14267  prmlem2  16455  83prm  16458  163prm  16460  317prm  16461  631prm  16462  2503lem2  16473  2503lem3  16474  4001lem2  16477  4001lem3  16478  4001prm  16480  hgt750lem  31924  hgt750lem2  31925  3cubeslem3l  39290  3cubeslem3r  39291  fmtno5lem4  43725  fmtno4nprmfac193  43743  m3prm  43761  m7prm  43771  nnsum3primesle9  43966  bgoldbtbndlem1  43977