Theorem 7p1e8 12504

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430  1c1 11214   + caddc 11216  7c7 12415  8c8 12416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-8 12424

This theorem is used by:  7t4e28  12943  9t9e81  12961  s8len  15069  prmlem2  17313  83prm  17316  163prm  17318  317prm  17319  631prm  17320  2503lem2  17331  2503lem3  17332  4001lem2  17335  4001lem3  17336  4001prm  17338  hgt750lem  35336  hgt750lem2  35337  lcmineqlem  43248  1p7e8  43460  3cubeslem3l  43842  3cubeslem3r  43843  resqrtvalex  44791  imsqrtvalex  44792  fmtno5lem4  48786  fmtno4nprmfac193  48804  m3prm  48822  m7prm  48830  nnsum3primesle9  49037  bgoldbtbndlem1  49048