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

Theorem 5p1e6 10738
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 10673 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2435 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6302   1c1 9541    + caddc 9543   5c5 10663   6c6 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-6 10673
This theorem is referenced by:  8t8e64  11146  9t7e63  11152  5recm6rec  11159  s6len  12985  2exp6OLD  15047  163prm  15084  631prm  15086  prmo6  15089  1259lem1  15090  1259lem3  15092  1259lem4  15093  2503lem1  15096  2503lem2  15097  4001lem1  15100  4001lem4  15103  4001prm  15104  log2ublem3  23861  log2ub  23862  fib6  29235  gboge7  38576  gbege6  38578  bgoldbwt  38590  nnsum3primesle9  38601
  Copyright terms: Public domain W3C validator