Theorem 7p1e8 12393

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410  1c1 11105   + caddc 11107  7c7 12304  8c8 12305

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-8 12313

This theorem is used by:  7t4e28  12831  9t9e81  12849  s8len  14945  prmlem2  17184  83prm  17187  163prm  17189  317prm  17190  631prm  17191  2503lem2  17202  2503lem3  17203  4001lem2  17206  4001lem3  17207  4001prm  17209  hgt750lem  35047  hgt750lem2  35048  lcmineqlem  42847  3cubeslem3l  43445  3cubeslem3r  43446  resqrtvalex  44399  imsqrtvalex  44400  fmtno5lem4  48336  fmtno4nprmfac193  48354  m3prm  48372  m7prm  48380  nnsum3primesle9  48587  bgoldbtbndlem1  48598