Theorem 7p1e8 12306

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  7c7 12222  8c8 12223

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 12231

This theorem is referenced by:  7t4e28  12736  9t9e81  12754  s8len  14845  prmlem2  17066  83prm  17069  163prm  17071  317prm  17072  631prm  17073  2503lem2  17084  2503lem3  17085  4001lem2  17088  4001lem3  17089  4001prm  17091  hgt750lem  34635  hgt750lem2  34636  lcmineqlem  42033  3cubeslem3l  42667  3cubeslem3r  42668  resqrtvalex  43627  imsqrtvalex  43628  fmtno5lem4  47550  fmtno4nprmfac193  47568  m3prm  47586  m7prm  47594  nnsum3primesle9  47788  bgoldbtbndlem1  47799