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

Theorem 6p1e7 11107
Description: 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
6p1e7 (6 + 1) = 7

Proof of Theorem 6p1e7
StepHypRef Expression
1 df-7 11035 . 2 7 = (6 + 1)
21eqcomi 2630 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6610  1c1 9888   + caddc 9890  6c6 11025  7c7 11026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-7 11035
This theorem is referenced by:  9t8e72  11620  s7len  13590  37prm  15759  163prm  15763  317prm  15764  631prm  15765  1259lem1  15769  1259lem3  15771  1259lem4  15772  1259lem5  15773  2503lem1  15775  2503lem2  15776  2503lem3  15777  2503prm  15778  4001lem1  15779  4001lem4  15782  4001prm  15783  log2ublem3  24588  log2ub  24589  fmtno2  40782  fmtno3  40783  fmtno4  40784  fmtno5lem4  40788  fmtno5  40789  fmtno4nprmfac193  40806  fmtno5fac  40814  127prm  40835  mod42tp1mod8  40839  gboge7  40967  bgoldbwt  40981  nnsum3primesle9  40992
  Copyright terms: Public domain W3C validator