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

Theorem 7p1e8 12309
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 12229 . 2 8 = (7 + 1)
21eqcomi 2746 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11059   + caddc 11061  7c7 12220  8c8 12221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-8 12229
This theorem is referenced by:  7t4e28  12736  9t9e81  12754  s8len  14799  prmlem2  16999  83prm  17002  163prm  17004  317prm  17005  631prm  17006  2503lem2  17017  2503lem3  17018  4001lem2  17021  4001lem3  17022  4001prm  17024  hgt750lem  33304  hgt750lem2  33305  lcmineqlem  40538  3cubeslem3l  41038  3cubeslem3r  41039  resqrtvalex  41991  imsqrtvalex  41992  fmtno5lem4  45822  fmtno4nprmfac193  45840  m3prm  45858  m7prm  45866  nnsum3primesle9  46060  bgoldbtbndlem1  46071
  Copyright terms: Public domain W3C validator