Theorem 7p1e8 12442

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  7c7 12353  8c8 12354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-8 12362

This theorem is referenced by:  7t4e28  12869  9t9e81  12887  s8len  14952  prmlem2  17167  83prm  17170  163prm  17172  317prm  17173  631prm  17174  2503lem2  17185  2503lem3  17186  4001lem2  17189  4001lem3  17190  4001prm  17192  hgt750lem  34628  hgt750lem2  34629  lcmineqlem  42009  3cubeslem3l  42642  3cubeslem3r  42643  resqrtvalex  43607  imsqrtvalex  43608  fmtno5lem4  47430  fmtno4nprmfac193  47448  m3prm  47466  m7prm  47474  nnsum3primesle9  47668  bgoldbtbndlem1  47679