Theorem 7p1e8 11944

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

Syntax hints:   = wceq 1543  (class class class)co 7191  1c1 10695   + caddc 10697  7c7 11855  8c8 11856

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 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-8 11864

This theorem is referenced by:  7t4e28  12369  9t9e81  12387  s8len  14433  prmlem2  16636  83prm  16639  163prm  16641  317prm  16642  631prm  16643  2503lem2  16654  2503lem3  16655  4001lem2  16658  4001lem3  16659  4001prm  16661  hgt750lem  32297  hgt750lem2  32298  lcmineqlem  39743  3cubeslem3l  40152  3cubeslem3r  40153  resqrtvalex  40870  imsqrtvalex  40871  fmtno5lem4  44624  fmtno4nprmfac193  44642  m3prm  44660  m7prm  44668  nnsum3primesle9  44862  bgoldbtbndlem1  44873