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

Theorem 5p1e6 12299
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 12219 . 2 6 = (5 + 1)
21eqcomi 2745 1 (5 + 1) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11051   + caddc 11053  5c5 12210  6c6 12211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-6 12219
This theorem is referenced by:  8t8e64  12738  9t7e63  12744  5recm6rec  12761  fldiv4p1lem1div2  13739  s6len  14789  163prm  16996  631prm  16998  1259lem1  17002  1259lem4  17005  2503lem1  17008  2503lem2  17009  4001lem1  17012  4001lem4  17015  4001prm  17016  log2ublem3  26296  log2ub  26297  fib6  32997  hgt750lemd  33252  hgt750lem2  33256  60gcd7e1  40453  12lcm5e60  40456  3lexlogpow5ineq1  40502  3lexlogpow5ineq5  40508  aks4d1p1  40524  3cubeslem3l  40987  fmtno5lem2  45718  fmtno5lem3  45719  fmtno5lem4  45720  fmtno4prmfac193  45737  fmtno4nprmfac193  45738  fmtno5faclem3  45745  flsqrt5  45758  127prm  45763  gbowge7  45927  gbege6  45929  sbgoldbwt  45941  nnsum3primesle9  45958
  Copyright terms: Public domain W3C validator