Theorem 7p1e8 12337

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  7c7 12253  8c8 12254

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-8 12262

This theorem is referenced by:  7t4e28  12767  9t9e81  12785  s8len  14876  prmlem2  17097  83prm  17100  163prm  17102  317prm  17103  631prm  17104  2503lem2  17115  2503lem3  17116  4001lem2  17119  4001lem3  17120  4001prm  17122  hgt750lem  34649  hgt750lem2  34650  lcmineqlem  42047  3cubeslem3l  42681  3cubeslem3r  42682  resqrtvalex  43641  imsqrtvalex  43642  fmtno5lem4  47561  fmtno4nprmfac193  47579  m3prm  47597  m7prm  47605  nnsum3primesle9  47799  bgoldbtbndlem1  47810