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

Theorem 5p1e6 10670
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 10605 . 2  |-  6  =  ( 5  +  1 )
21eqcomi 2456 1  |-  ( 5  +  1 )  =  6
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281   1c1 9496    + caddc 9498   5c5 10595   6c6 10596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-6 10605
This theorem is referenced by:  8t8e64  11080  9t7e63  11086  s6len  12841  2exp6OLD  14555  163prm  14592  631prm  14594  1259lem1  14595  1259lem3  14597  1259lem4  14598  2503lem1  14601  2503lem2  14602  4001lem1  14605  4001lem4  14608  4001prm  14609  log2ublem3  23257  log2ub  23258  fib6  28323  5recm6rec  29092
  Copyright terms: Public domain W3C validator