Theorem 7p1e8 12330

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  7c7 12246  8c8 12247

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 12255

This theorem is referenced by:  7t4e28  12760  9t9e81  12778  s8len  14869  prmlem2  17090  83prm  17093  163prm  17095  317prm  17096  631prm  17097  2503lem2  17108  2503lem3  17109  4001lem2  17112  4001lem3  17113  4001prm  17115  hgt750lem  34642  hgt750lem2  34643  lcmineqlem  42040  3cubeslem3l  42674  3cubeslem3r  42675  resqrtvalex  43634  imsqrtvalex  43635  fmtno5lem4  47557  fmtno4nprmfac193  47575  m3prm  47593  m7prm  47601  nnsum3primesle9  47795  bgoldbtbndlem1  47806