Theorem 7p1e8 12320

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

Syntax hints:   = wceq 1548  (class class class)co 7360  1c1 11034   + caddc 11036  7c7 12236  8c8 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-8 12245

This theorem is referenced by:  7t4e28  12750  9t9e81  12768  s8len  14860  prmlem2  17085  83prm  17088  163prm  17090  317prm  17091  631prm  17092  2503lem2  17103  2503lem3  17104  4001lem2  17107  4001lem3  17108  4001prm  17110  hgt750lem  34847  hgt750lem2  34848  lcmineqlem  42552  3cubeslem3l  43150  3cubeslem3r  43151  resqrtvalex  44104  imsqrtvalex  44105  fmtno5lem4  48048  fmtno4nprmfac193  48066  m3prm  48084  m7prm  48092  nnsum3primesle9  48299  bgoldbtbndlem1  48310