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

Theorem 5p1e6 10737
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 10672 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2460 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444  (class class class)co 6290   1c1 9540    + caddc 9542   5c5 10662   6c6 10663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-6 10672
This theorem is referenced by:  8t8e64  11145  9t7e63  11151  5recm6rec  11158  s6len  12995  2exp6OLD  15059  163prm  15096  631prm  15098  prmo6  15101  1259lem1  15102  1259lem3  15104  1259lem4  15105  2503lem1  15108  2503lem2  15109  4001lem1  15112  4001lem4  15115  4001prm  15116  log2ublem3  23874  log2ub  23875  fib6  29239  gboge7  38864  gbege6  38866  bgoldbwt  38878  nnsum3primesle9  38889
  Copyright terms: Public domain W3C validator