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

Theorem 5p1e6 11032
 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 10960 . 2 6 = (5 + 1)
21eqcomi 2619 1 (5 + 1) = 6
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  5c5 10950  6c6 10951 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-6 10960 This theorem is referenced by:  8t8e64  11538  9t7e63  11544  5recm6rec  11562  fldiv4p1lem1div2  12498  s6len  13496  163prm  15670  631prm  15672  prmo6  15675  1259lem1  15676  1259lem4  15679  2503lem1  15682  2503lem2  15683  4001lem1  15686  4001lem4  15689  4001prm  15690  log2ublem3  24475  log2ub  24476  fib6  29795  fmtno5lem2  40004  fmtno5lem3  40005  fmtno5lem4  40006  fmtno4prmfac193  40023  fmtno4nprmfac193  40024  fmtno5faclem3  40031  flsqrt5  40047  127prm  40053  gboge7  40185  gbege6  40187  bgoldbwt  40199  nnsum3primesle9  40210
 Copyright terms: Public domain W3C validator