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

Theorem 5p1e6 11505
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 11418 . 2 6 = (5 + 1)
21eqcomi 2834 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  (class class class)co 6905  1c1 10253   + caddc 10255  5c5 11409  6c6 11410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-6 11418
This theorem is referenced by:  8t8e64  11944  9t7e63  11950  5recm6rec  11967  fldiv4p1lem1div2  12931  s6len  14022  163prm  16197  631prm  16199  prmo6  16202  1259lem1  16203  1259lem4  16206  2503lem1  16209  2503lem2  16210  4001lem1  16213  4001lem4  16216  4001prm  16217  log2ublem3  25088  log2ub  25089  fib6  31003  hgt750lemd  31264  hgt750lem2  31268  fmtno5lem2  42289  fmtno5lem3  42290  fmtno5lem4  42291  fmtno4prmfac193  42308  fmtno4nprmfac193  42309  fmtno5faclem3  42316  flsqrt5  42332  127prm  42338  gbowge7  42474  gbege6  42476  sbgoldbwt  42488  nnsum3primesle9  42505
  Copyright terms: Public domain W3C validator