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

Theorem 5p1e6 9866
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 9824 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2300 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   5c5 9814   6c6 9815
This theorem is referenced by:  8t8e64  10234  9t7e63  10240  s6len  11560  2exp6  13117  163prm  13142  631prm  13144  1259lem1  13145  1259lem3  13147  1259lem4  13148  2503lem1  13151  2503lem2  13152  4001lem1  13155  4001lem4  13158  4001prm  13159  log2ublem3  20260  log2ub  20261  5recm6rec  24116
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-6 9824
  Copyright terms: Public domain W3C validator