Theorem 7p1e8 12415

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  7c7 12326  8c8 12327

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 2708

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

This theorem is referenced by:  7t4e28  12844  9t9e81  12862  s8len  14942  prmlem2  17157  83prm  17160  163prm  17162  317prm  17163  631prm  17164  2503lem2  17175  2503lem3  17176  4001lem2  17179  4001lem3  17180  4001prm  17182  hgt750lem  34666  hgt750lem2  34667  lcmineqlem  42053  3cubeslem3l  42697  3cubeslem3r  42698  resqrtvalex  43658  imsqrtvalex  43659  fmtno5lem4  47543  fmtno4nprmfac193  47561  m3prm  47579  m7prm  47587  nnsum3primesle9  47781  bgoldbtbndlem1  47792