Theorem 7p1e8 11787

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   + caddc 10540  7c7 11698  8c8 11699

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-8 11707

This theorem is referenced by:  7t4e28  12210  9t9e81  12228  s8len  14265  prmlem2  16453  83prm  16456  163prm  16458  317prm  16459  631prm  16460  2503lem2  16471  2503lem3  16472  4001lem2  16475  4001lem3  16476  4001prm  16478  hgt750lem  31922  hgt750lem2  31923  3cubeslem3l  39303  3cubeslem3r  39304  fmtno5lem4  43738  fmtno4nprmfac193  43756  m3prm  43774  m7prm  43784  nnsum3primesle9  43979  bgoldbtbndlem1  43990