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

Theorem 5p1e6 11773
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 11693 . 2 6 = (5 + 1)
21eqcomi 2830 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  1c1 10527   + caddc 10529  5c5 11684  6c6 11685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-6 11693
This theorem is referenced by:  8t8e64  12208  9t7e63  12214  5recm6rec  12231  fldiv4p1lem1div2  13195  s6len  14253  163prm  16448  631prm  16450  1259lem1  16454  1259lem4  16457  2503lem1  16460  2503lem2  16461  4001lem1  16464  4001lem4  16467  4001prm  16468  log2ublem3  25454  log2ub  25455  fib6  31564  hgt750lemd  31819  hgt750lem2  31823  3cubeslem3l  39163  fmtno5lem2  43563  fmtno5lem3  43564  fmtno5lem4  43565  fmtno4prmfac193  43582  fmtno4nprmfac193  43583  fmtno5faclem3  43590  flsqrt5  43604  127prm  43610  gbowge7  43775  gbege6  43777  sbgoldbwt  43789  nnsum3primesle9  43806
  Copyright terms: Public domain W3C validator