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

Theorem 3p1e4 9864
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 9822 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2300 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   3c3 9812   4c4 9813
This theorem is referenced by:  7t6e42  10226  8t5e40  10231  9t5e45  10238  fac4  11312  hash4  11389  s4len  11558  2exp16  13119  43prm  13139  83prm  13140  317prm  13143  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  2503lem1  13151  2503lem2  13152  4001lem1  13155  4001lem2  13156  4001lem4  13158  4001prm  13159  sincos6thpi  19899  binom4  20162  quartlem1  20169  log2ublem3  20260  log2ub  20261  bclbnd  20535  ex-opab  20835  4bc3eq4  24113  bpoly4  24866  lhe4.4ex1a  27649  stoweidlem26  27878  4cycl4v4e  28412  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-4 9822
  Copyright terms: Public domain W3C validator