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

Theorem 5p1e6 11115
Description: 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
5p1e6 (5 + 1) = 6

Proof of Theorem 5p1e6
StepHypRef Expression
1 df-6 11043 . 2 6 = (5 + 1)
21eqcomi 2630 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6615  1c1 9897   + caddc 9899  5c5 11033  6c6 11034
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-6 11043
This theorem is referenced by:  8t8e64  11622  9t7e63  11628  5recm6rec  11646  fldiv4p1lem1div2  12592  s6len  13598  163prm  15775  631prm  15777  prmo6  15780  1259lem1  15781  1259lem4  15784  2503lem1  15787  2503lem2  15788  4001lem1  15791  4001lem4  15794  4001prm  15795  log2ublem3  24609  log2ub  24610  fib6  30291  fmtno5lem2  40795  fmtno5lem3  40796  fmtno5lem4  40797  fmtno4prmfac193  40814  fmtno4nprmfac193  40815  fmtno5faclem3  40822  flsqrt5  40838  127prm  40844  gboge7  40976  gbege6  40978  bgoldbwt  40990  nnsum3primesle9  41001
  Copyright terms: Public domain W3C validator