Theorem 7p1e8 12389

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

Syntax hints:   = wceq 1540  (class class class)co 7405  1c1 11130   + caddc 11132  7c7 12300  8c8 12301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-8 12309

This theorem is referenced by:  7t4e28  12819  9t9e81  12837  s8len  14922  prmlem2  17139  83prm  17142  163prm  17144  317prm  17145  631prm  17146  2503lem2  17157  2503lem3  17158  4001lem2  17161  4001lem3  17162  4001prm  17164  hgt750lem  34683  hgt750lem2  34684  lcmineqlem  42065  3cubeslem3l  42709  3cubeslem3r  42710  resqrtvalex  43669  imsqrtvalex  43670  fmtno5lem4  47570  fmtno4nprmfac193  47588  m3prm  47606  m7prm  47614  nnsum3primesle9  47808  bgoldbtbndlem1  47819