Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  7p1e8 Structured version   Visualization version   GIF version

Theorem 7p1e8 11034
 Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
7p1e8 (7 + 1) = 8

Proof of Theorem 7p1e8
StepHypRef Expression
1 df-8 10962 . 2 8 = (7 + 1)
21eqcomi 2619 1 (7 + 1) = 8
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  7c7 10952  8c8 10953 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-8 10962 This theorem is referenced by:  7t4e28  11526  9t9e81  11546  s8len  13498  prmlem2  15665  83prm  15668  163prm  15670  317prm  15671  631prm  15672  2503lem2  15683  2503lem3  15684  4001lem2  15687  4001lem3  15688  4001prm  15690  fmtno5lem4  40006  fmtno4nprmfac193  40024  m3prm  40044  m7prm  40054  nnsum3primesle9  40210  bgoldbtbndlem1  40221
 Copyright terms: Public domain W3C validator