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 2741	1 ⊢ (7 + 1) = 8

Syntax hints:   = wceq 1541  (class class class)co 7408  1c1 11110   + caddc 11112  7c7 12271  8c8 12272

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-8 12280

This theorem is referenced by:  7t4e28  12787  9t9e81  12805  s8len  14853  prmlem2  17052  83prm  17055  163prm  17057  317prm  17058  631prm  17059  2503lem2  17070  2503lem3  17071  4001lem2  17074  4001lem3  17075  4001prm  17077  hgt750lem  33658  hgt750lem2  33659  lcmineqlem  40912  3cubeslem3l  41414  3cubeslem3r  41415  resqrtvalex  42386  imsqrtvalex  42387  fmtno5lem4  46214  fmtno4nprmfac193  46232  m3prm  46250  m7prm  46258  nnsum3primesle9  46452  bgoldbtbndlem1  46463