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

Theorem 6p1e7 12300
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 12220 . 2 7 = (6 + 1)
21eqcomi 2745 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11051   + caddc 11053  6c6 12211  7c7 12212
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-7 12220
This theorem is referenced by:  9t8e72  12745  s7len  14790  37prm  16992  163prm  16996  317prm  16997  631prm  16998  1259lem1  17002  1259lem3  17004  1259lem4  17005  1259lem5  17006  2503lem1  17008  2503lem2  17009  2503lem3  17010  2503prm  17011  4001lem1  17012  4001lem4  17015  4001prm  17016  log2ublem3  26296  log2ub  26297  hgt750lemd  33201  hgt750lem2  33205  3exp7  40500  3lexlogpow5ineq1  40501  235t711  40782  ex-decpmul  40783  3cubeslem3l  40986  3cubeslem3r  40987  fmtno2  45713  fmtno3  45714  fmtno4  45715  fmtno5lem4  45719  fmtno5  45720  fmtno4nprmfac193  45737  fmtno5fac  45745  127prm  45762  mod42tp1mod8  45765  2exp340mod341  45896  gbowge7  45926  sbgoldbwt  45940  nnsum3primesle9  45957
  Copyright terms: Public domain W3C validator