Theorem 7p1e8 11589

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

Syntax hints:   = wceq 1507  (class class class)co 6970  1c1 10328   + caddc 10330  7c7 11493  8c8 11494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-8 11502

This theorem is referenced by:  7t4e28  12017  9t9e81  12035  s8len  14117  prmlem2  16299  83prm  16302  163prm  16304  317prm  16305  631prm  16306  2503lem2  16317  2503lem3  16318  4001lem2  16321  4001lem3  16322  4001prm  16324  hgt750lem  31531  hgt750lem2  31532  fmtno5lem4  43026  fmtno4nprmfac193  43044  m3prm  43062  m7prm  43072  nnsum3primesle9  43267  bgoldbtbndlem1  43278