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

Theorem 5p1e6 12301
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 12221 . 2 6 = (5 + 1)
21eqcomi 2746 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7358  1c1 11053   + caddc 11055  5c5 12212  6c6 12213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-6 12221
This theorem is referenced by:  8t8e64  12740  9t7e63  12746  5recm6rec  12763  fldiv4p1lem1div2  13741  s6len  14791  163prm  16998  631prm  17000  1259lem1  17004  1259lem4  17007  2503lem1  17010  2503lem2  17011  4001lem1  17014  4001lem4  17017  4001prm  17018  log2ublem3  26301  log2ub  26302  fib6  33009  hgt750lemd  33264  hgt750lem2  33268  60gcd7e1  40465  12lcm5e60  40468  3lexlogpow5ineq1  40514  3lexlogpow5ineq5  40520  aks4d1p1  40536  3cubeslem3l  41012  fmtno5lem2  45753  fmtno5lem3  45754  fmtno5lem4  45755  fmtno4prmfac193  45772  fmtno4nprmfac193  45773  fmtno5faclem3  45780  flsqrt5  45793  127prm  45798  gbowge7  45962  gbege6  45964  sbgoldbwt  45976  nnsum3primesle9  45993
  Copyright terms: Public domain W3C validator