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

Theorem 3p1e4 10650
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 10585 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2473 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374  (class class class)co 6275   1c1 9482    + caddc 9484   3c3 10575   4c4 10576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-cleq 2452  df-4 10585
This theorem is referenced by:  7t6e42  11051  8t5e40  11056  9t5e45  11063  fac4  12316  hash4  12425  s4len  12807  2exp16  14422  43prm  14454  83prm  14455  317prm  14458  1259lem2  14461  1259lem3  14462  1259lem4  14463  1259lem5  14464  2503lem1  14466  2503lem2  14467  4001lem1  14470  4001lem2  14471  4001lem4  14473  4001prm  14474  sincos6thpi  22634  binom4  22902  quartlem1  22909  log2ublem3  23000  log2ub  23001  bclbnd  23276  4cycl4v4e  24328  4cycl4dv4e  24330  ex-opab  24816  fib4  27969  fib5  27970  4bc3eq4  28572  bpoly4  29384  lhe4.4ex1a  30789  stoweidlem26  31281  stoweidlem34  31289
  Copyright terms: Public domain W3C validator