Theorem 7p1e8 12122

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

Syntax hints:   = wceq 1539  (class class class)co 7275  1c1 10872   + caddc 10874  7c7 12033  8c8 12034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-8 12042

This theorem is referenced by:  7t4e28  12548  9t9e81  12566  s8len  14616  prmlem2  16821  83prm  16824  163prm  16826  317prm  16827  631prm  16828  2503lem2  16839  2503lem3  16840  4001lem2  16843  4001lem3  16844  4001prm  16846  hgt750lem  32631  hgt750lem2  32632  lcmineqlem  40060  3cubeslem3l  40508  3cubeslem3r  40509  resqrtvalex  41253  imsqrtvalex  41254  fmtno5lem4  45008  fmtno4nprmfac193  45026  m3prm  45044  m7prm  45052  nnsum3primesle9  45246  bgoldbtbndlem1  45257