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

Theorem 6p1e7 12234
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 12154 . 2 7 = (6 + 1)
21eqcomi 2746 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7349  1c1 10985   + caddc 10987  6c6 12145  7c7 12146
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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-7 12154
This theorem is referenced by:  9t8e72  12678  s7len  14722  37prm  16927  163prm  16931  317prm  16932  631prm  16933  1259lem1  16937  1259lem3  16939  1259lem4  16940  1259lem5  16941  2503lem1  16943  2503lem2  16944  2503lem3  16945  2503prm  16946  4001lem1  16947  4001lem4  16950  4001prm  16951  log2ublem3  26220  log2ub  26221  hgt750lemd  33034  hgt750lem2  33038  3exp7  40405  3lexlogpow5ineq1  40406  235t711  40673  ex-decpmul  40674  3cubeslem3l  40874  3cubeslem3r  40875  fmtno2  45491  fmtno3  45492  fmtno4  45493  fmtno5lem4  45497  fmtno5  45498  fmtno4nprmfac193  45515  fmtno5fac  45523  127prm  45540  mod42tp1mod8  45543  2exp340mod341  45674  gbowge7  45704  sbgoldbwt  45718  nnsum3primesle9  45735
  Copyright terms: Public domain W3C validator