Theorem 7p1e8 12293

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

Syntax hints:   = wceq 1542  (class class class)co 7360  1c1 11031   + caddc 11033  7c7 12209  8c8 12210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-8 12218

This theorem is referenced by:  7t4e28  12722  9t9e81  12740  s8len  14830  prmlem2  17051  83prm  17054  163prm  17056  317prm  17057  631prm  17058  2503lem2  17069  2503lem3  17070  4001lem2  17073  4001lem3  17074  4001prm  17076  hgt750lem  34810  hgt750lem2  34811  lcmineqlem  42374  3cubeslem3l  42995  3cubeslem3r  42996  resqrtvalex  43953  imsqrtvalex  43954  fmtno5lem4  47869  fmtno4nprmfac193  47887  m3prm  47905  m7prm  47913  nnsum3primesle9  48107  bgoldbtbndlem1  48118