Theorem 7p1e8 12407

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

Syntax hints:   = wceq 1534  (class class class)co 7416  1c1 11150   + caddc 11152  7c7 12318  8c8 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-8 12327

This theorem is referenced by:  7t4e28  12834  9t9e81  12852  s8len  14907  prmlem2  17117  83prm  17120  163prm  17122  317prm  17123  631prm  17124  2503lem2  17135  2503lem3  17136  4001lem2  17139  4001lem3  17140  4001prm  17142  hgt750lem  34510  hgt750lem2  34511  lcmineqlem  41764  3cubeslem3l  42380  3cubeslem3r  42381  resqrtvalex  43349  imsqrtvalex  43350  fmtno5lem4  47164  fmtno4nprmfac193  47182  m3prm  47200  m7prm  47208  nnsum3primesle9  47402  bgoldbtbndlem1  47413