Theorem 7p1e8 12391

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

Syntax hints:   = wceq 1534  (class class class)co 7420  1c1 11139   + caddc 11141  7c7 12302  8c8 12303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-8 12311

This theorem is referenced by:  7t4e28  12818  9t9e81  12836  s8len  14886  prmlem2  17088  83prm  17091  163prm  17093  317prm  17094  631prm  17095  2503lem2  17106  2503lem3  17107  4001lem2  17110  4001lem3  17111  4001prm  17113  hgt750lem  34283  hgt750lem2  34284  lcmineqlem  41523  3cubeslem3l  42106  3cubeslem3r  42107  resqrtvalex  43075  imsqrtvalex  43076  fmtno5lem4  46896  fmtno4nprmfac193  46914  m3prm  46932  m7prm  46940  nnsum3primesle9  47134  bgoldbtbndlem1  47145