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

Theorem 5p1e6 11356
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 11284 . 2 6 = (5 + 1)
21eqcomi 2779 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  (class class class)co 6792  1c1 10138   + caddc 10140  5c5 11274  6c6 11275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-cleq 2763  df-6 11284
This theorem is referenced by:  8t8e64  11862  9t7e63  11868  5recm6rec  11886  fldiv4p1lem1div2  12843  s6len  13854  163prm  16038  631prm  16040  prmo6  16043  1259lem1  16044  1259lem4  16047  2503lem1  16050  2503lem2  16051  4001lem1  16054  4001lem4  16057  4001prm  16058  log2ublem3  24895  log2ub  24896  fib6  30802  hgt750lemd  31060  hgt750lem2  31064  fmtno5lem2  41984  fmtno5lem3  41985  fmtno5lem4  41986  fmtno4prmfac193  42003  fmtno4nprmfac193  42004  fmtno5faclem3  42011  flsqrt5  42027  127prm  42033  gbowge7  42169  gbege6  42171  sbgoldbwt  42183  nnsum3primesle9  42200
  Copyright terms: Public domain W3C validator