Theorem 7p1e8 12360

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

Syntax hints:   = wceq 1533  (class class class)co 7402  1c1 11108   + caddc 11110  7c7 12271  8c8 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-8 12280

This theorem is referenced by:  7t4e28  12787  9t9e81  12805  s8len  14856  prmlem2  17058  83prm  17061  163prm  17063  317prm  17064  631prm  17065  2503lem2  17076  2503lem3  17077  4001lem2  17080  4001lem3  17081  4001prm  17083  hgt750lem  34181  hgt750lem2  34182  lcmineqlem  41423  3cubeslem3l  41974  3cubeslem3r  41975  resqrtvalex  42945  imsqrtvalex  42946  fmtno5lem4  46769  fmtno4nprmfac193  46787  m3prm  46805  m7prm  46813  nnsum3primesle9  47007  bgoldbtbndlem1  47018