Theorem 7p1e8 12272

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  7c7 12188  8c8 12189

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  7t4e28  12702  9t9e81  12720  s8len  14810  prmlem2  17031  83prm  17034  163prm  17036  317prm  17037  631prm  17038  2503lem2  17049  2503lem3  17050  4001lem2  17053  4001lem3  17054  4001prm  17056  hgt750lem  34625  hgt750lem2  34626  lcmineqlem  42035  3cubeslem3l  42669  3cubeslem3r  42670  resqrtvalex  43628  imsqrtvalex  43629  fmtno5lem4  47550  fmtno4nprmfac193  47568  m3prm  47586  m7prm  47594  nnsum3primesle9  47788  bgoldbtbndlem1  47799