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

Theorem 5p1e6 11779
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 11699 . 2 6 = (5 + 1)
21eqcomi 2833 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7146  1c1 10532   + caddc 10534  5c5 11690  6c6 11691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-6 11699
This theorem is referenced by:  8t8e64  12214  9t7e63  12220  5recm6rec  12237  fldiv4p1lem1div2  13207  s6len  14261  163prm  16456  631prm  16458  1259lem1  16462  1259lem4  16465  2503lem1  16468  2503lem2  16469  4001lem1  16472  4001lem4  16475  4001prm  16476  log2ublem3  25532  log2ub  25533  fib6  31691  hgt750lemd  31946  hgt750lem2  31950  60gcd7e1  39201  12lcm5e60  39204  3cubeslem3l  39483  fmtno5lem2  43937  fmtno5lem3  43938  fmtno5lem4  43939  fmtno4prmfac193  43956  fmtno4nprmfac193  43957  fmtno5faclem3  43964  flsqrt5  43977  127prm  43982  gbowge7  44147  gbege6  44149  sbgoldbwt  44161  nnsum3primesle9  44178
  Copyright terms: Public domain W3C validator