Theorem 7p1e8 12269

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  7c7 12185  8c8 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-8 12194

This theorem is referenced by:  7t4e28  12699  9t9e81  12717  s8len  14810  prmlem2  17031  83prm  17034  163prm  17036  317prm  17037  631prm  17038  2503lem2  17049  2503lem3  17050  4001lem2  17053  4001lem3  17054  4001prm  17056  hgt750lem  34664  hgt750lem2  34665  lcmineqlem  42155  3cubeslem3l  42789  3cubeslem3r  42790  resqrtvalex  43748  imsqrtvalex  43749  fmtno5lem4  47666  fmtno4nprmfac193  47684  m3prm  47702  m7prm  47710  nnsum3primesle9  47904  bgoldbtbndlem1  47915