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

Theorem 6p1e7 12235
Description: 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
6p1e7 (6 + 1) = 7

Proof of Theorem 6p1e7
StepHypRef Expression
1 df-7 12155 . 2 7 = (6 + 1)
21eqcomi 2747 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  1c1 10986   + caddc 10988  6c6 12146  7c7 12147
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 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-7 12155
This theorem is referenced by:  9t8e72  12679  s7len  14723  37prm  16928  163prm  16932  317prm  16933  631prm  16934  1259lem1  16938  1259lem3  16940  1259lem4  16941  1259lem5  16942  2503lem1  16944  2503lem2  16945  2503lem3  16946  2503prm  16947  4001lem1  16948  4001lem4  16951  4001prm  16952  log2ublem3  26220  log2ub  26221  hgt750lemd  33022  hgt750lem2  33026  3exp7  40396  3lexlogpow5ineq1  40397  235t711  40652  ex-decpmul  40653  3cubeslem3l  40843  3cubeslem3r  40844  fmtno2  45460  fmtno3  45461  fmtno4  45462  fmtno5lem4  45466  fmtno5  45467  fmtno4nprmfac193  45484  fmtno5fac  45492  127prm  45509  mod42tp1mod8  45512  2exp340mod341  45643  gbowge7  45673  sbgoldbwt  45687  nnsum3primesle9  45704
  Copyright terms: Public domain W3C validator