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

Theorem 3p1e4 11774
Description: 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
3p1e4 (3 + 1) = 4

Proof of Theorem 3p1e4
StepHypRef Expression
1 df-4 11694 . 2 4 = (3 + 1)
21eqcomi 2828 1 (3 + 1) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1531  (class class class)co 7148  1c1 10530   + caddc 10532  3c3 11685  4c4 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-4 11694
This theorem is referenced by:  7t6e42  12203  8t5e40  12208  9t5e45  12215  fac4  13633  hash4  13760  s4len  14253  bpoly4  15405  2exp16  16416  43prm  16447  83prm  16448  317prm  16451  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  4001lem1  16466  4001lem2  16467  4001lem4  16469  4001prm  16470  binom4  25420  quartlem1  25427  log2ublem3  25518  log2ub  25519  bclbnd  25848  addsqnreup  26011  tgcgr4  26309  upgr4cycl4dv4e  27956  ex-opab  28203  ex-ind-dvds  28232  fib4  31655  fib5  31656  hgt750lem  31915  hgt750lem2  31916  235t711  39168  3cubeslem3l  39274  3cubeslem3r  39275  inductionexd  40496  lhe4.4ex1a  40652  stoweidlem26  42302  stoweidlem34  42310  smfmullem2  43058  fmtno5lem4  43709  fmtno5  43710  fmtno5faclem2  43733  3ndvds4  43749  139prmALT  43750  31prm  43751  m5prm  43752  11t31e341  43888  2exp340mod341  43889  8exp8mod9  43892  sbgoldbalt  43937  sbgoldbo  43943  nnsum3primesle9  43950  nnsum4primeseven  43956  nnsum4primesevenALTV  43957
  Copyright terms: Public domain W3C validator