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

Theorem 3p1e4 10667
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 10602 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2456 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281   1c1 9496    + caddc 9498   3c3 10592   4c4 10593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-4 10602
This theorem is referenced by:  7t6e42  11070  8t5e40  11075  9t5e45  11082  fac4  12340  hash4  12451  s4len  12836  2exp16  14452  43prm  14484  83prm  14485  317prm  14488  1259lem2  14491  1259lem3  14492  1259lem4  14493  1259lem5  14494  2503lem1  14496  2503lem2  14497  4001lem1  14500  4001lem2  14501  4001lem4  14503  4001prm  14504  sincos6thpi  22780  binom4  23053  quartlem1  23060  log2ublem3  23151  log2ub  23152  bclbnd  23427  4cycl4v4e  24538  4cycl4dv4e  24540  ex-opab  25025  ex-ind-dvds  25042  fib4  28216  fib5  28217  4bc3eq4  28984  bpoly4  29796  lhe4.4ex1a  31210  stoweidlem26  31697  stoweidlem34  31705  inductionexd  37637
  Copyright terms: Public domain W3C validator