Theorem 7p1e8 12287

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  7c7 12203  8c8 12204

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 2123  ax-ext 2706

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

This theorem is referenced by:  7t4e28  12716  9t9e81  12734  s8len  14824  prmlem2  17045  83prm  17048  163prm  17050  317prm  17051  631prm  17052  2503lem2  17063  2503lem3  17064  4001lem2  17067  4001lem3  17068  4001prm  17070  hgt750lem  34757  hgt750lem2  34758  lcmineqlem  42245  3cubeslem3l  42870  3cubeslem3r  42871  resqrtvalex  43828  imsqrtvalex  43829  fmtno5lem4  47744  fmtno4nprmfac193  47762  m3prm  47780  m7prm  47788  nnsum3primesle9  47982  bgoldbtbndlem1  47993