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

Theorem 3p1e4 10106
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 10062 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2442 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083   1c1 8993    + caddc 8995   3c3 10052   4c4 10053
This theorem is referenced by:  7t6e42  10470  8t5e40  10475  9t5e45  10482  fac4  11576  hash4  11678  s4len  11858  2exp16  13426  43prm  13446  83prm  13447  317prm  13450  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  2503lem1  13458  2503lem2  13459  4001lem1  13462  4001lem2  13463  4001lem4  13465  4001prm  13466  sincos6thpi  20425  binom4  20692  quartlem1  20699  log2ublem3  20790  log2ub  20791  bclbnd  21066  4cycl4v4e  21655  4cycl4dv4e  21657  ex-opab  21742  4bc3eq4  25205  bpoly4  26107  lhe4.4ex1a  27525  stoweidlem26  27753  stoweidlem34  27761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-4 10062
  Copyright terms: Public domain W3C validator