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

Theorem 5p1e6 10688
Description: 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
5p1e6

Proof of Theorem 5p1e6
StepHypRef Expression
1 df-6 10623 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  5c5 10613  6c6 10614
This theorem is referenced by:  8t8e64  11098  9t7e63  11104  s6len  12859  2exp6OLD  14573  163prm  14610  631prm  14612  1259lem1  14613  1259lem3  14615  1259lem4  14616  2503lem1  14619  2503lem2  14620  4001lem1  14623  4001lem4  14626  4001prm  14627  log2ublem3  23279  log2ub  23280  fib6  28345  5recm6rec  29114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-6 10623
  Copyright terms: Public domain W3C validator