Theorem 7p1e8 12435

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7415  1c1 11147   + caddc 11149  7c7 12346  8c8 12347

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-8 12355

This theorem is used by:  7t4e28  12874  9t9e81  12892  s8len  14996  prmlem2  17234  83prm  17237  163prm  17239  317prm  17240  631prm  17241  2503lem2  17252  2503lem3  17253  4001lem2  17256  4001lem3  17257  4001prm  17259  hgt750lem  35189  hgt750lem2  35190  lcmineqlem  42932  1p7e8  43144  3cubeslem3l  43545  3cubeslem3r  43546  resqrtvalex  44499  imsqrtvalex  44500  fmtno5lem4  48473  fmtno4nprmfac193  48491  m3prm  48509  m7prm  48517  nnsum3primesle9  48724  bgoldbtbndlem1  48735