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

Theorem 5p1e6 10663
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 10598 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2480 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6284   1c1 9493    + caddc 9495   5c5 10588   6c6 10589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-6 10598
This theorem is referenced by:  8t8e64  11070  9t7e63  11076  s6len  12822  2exp6  14431  163prm  14468  631prm  14470  1259lem1  14471  1259lem3  14473  1259lem4  14474  2503lem1  14477  2503lem2  14478  4001lem1  14481  4001lem4  14484  4001prm  14485  log2ublem3  23035  log2ub  23036  fib6  28013  5recm6rec  28617
  Copyright terms: Public domain W3C validator