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

Theorem 5p1e6 10108
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 10064 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2442 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083   1c1 8993    + caddc 8995   5c5 10054   6c6 10055
This theorem is referenced by:  8t8e64  10478  9t7e63  10484  s6len  11860  2exp6  13424  163prm  13449  631prm  13451  1259lem1  13452  1259lem3  13454  1259lem4  13455  2503lem1  13458  2503lem2  13459  4001lem1  13462  4001lem4  13465  4001prm  13466  log2ublem3  20790  log2ub  20791  5recm6rec  25208
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-6 10064
  Copyright terms: Public domain W3C validator