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  34789  hgt750lem2  34790  lcmineqlem  42343  3cubeslem3l  42964  3cubeslem3r  42965  resqrtvalex  43922  imsqrtvalex  43923  fmtno5lem4  47838  fmtno4nprmfac193  47856  m3prm  47874  m7prm  47882  nnsum3primesle9  48076  bgoldbtbndlem1  48087