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

Theorem 3p1e4 9848
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 9806 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2287 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   3c3 9796   4c4 9797
This theorem is referenced by:  7t6e42  10210  8t5e40  10215  9t5e45  10222  fac4  11296  hash4  11373  s4len  11542  2exp16  13103  43prm  13123  83prm  13124  317prm  13127  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  4001lem1  13139  4001lem2  13140  4001lem4  13142  4001prm  13143  sincos6thpi  19883  binom4  20146  quartlem1  20153  log2ublem3  20244  log2ub  20245  bclbnd  20519  ex-opab  20819  4bc3eq4  24098  bpoly4  24794  lhe4.4ex1a  27546  stoweidlem26  27775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-4 9806
  Copyright terms: Public domain W3C validator