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

Theorem 6p1e7 11779
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 11699 . 2 7 = (6 + 1)
21eqcomi 2835 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7150  1c1 10532   + caddc 10534  6c6 11690  7c7 11691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-7 11699
This theorem is referenced by:  9t8e72  12220  s7len  14259  37prm  16449  163prm  16453  317prm  16454  631prm  16455  1259lem1  16459  1259lem3  16461  1259lem4  16462  1259lem5  16463  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem4  16472  4001prm  16473  log2ublem3  25459  log2ub  25460  hgt750lemd  31824  hgt750lem2  31828  235t711  39061  ex-decpmul  39062  3cubeslem3l  39167  3cubeslem3r  39168  fmtno2  43563  fmtno3  43564  fmtno4  43565  fmtno5lem4  43569  fmtno5  43570  fmtno4nprmfac193  43587  fmtno5fac  43595  127prm  43614  mod42tp1mod8  43618  2exp340mod341  43749  gbowge7  43779  sbgoldbwt  43793  nnsum3primesle9  43810
  Copyright terms: Public domain W3C validator