Theorem 7p1e8 12491

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203  7c7 12402  8c8 12403

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 2733

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

This theorem is used by:  7t4e28  12930  9t9e81  12948  s8len  15054  prmlem2  17298  83prm  17301  163prm  17303  317prm  17304  631prm  17305  2503lem2  17316  2503lem3  17317  4001lem2  17320  4001lem3  17321  4001prm  17323  hgt750lem  35280  hgt750lem2  35281  lcmineqlem  43102  1p7e8  43314  3cubeslem3l  43696  3cubeslem3r  43697  resqrtvalex  44644  imsqrtvalex  44645  fmtno5lem4  48640  fmtno4nprmfac193  48658  m3prm  48676  m7prm  48684  nnsum3primesle9  48891  bgoldbtbndlem1  48902