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

Theorem 3p1e4 10657
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 10592 . 2  |-  4  =  ( 3  +  1 )
21eqcomi 2467 1  |-  ( 3  +  1 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398  (class class class)co 6270   1c1 9482    + caddc 9484   3c3 10582   4c4 10583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-4 10592
This theorem is referenced by:  7t6e42  11062  8t5e40  11067  9t5e45  11074  fac4  12343  hash4  12456  s4len  12848  2exp16  14659  43prm  14691  83prm  14692  317prm  14695  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  2503lem1  14703  2503lem2  14704  4001lem1  14707  4001lem2  14708  4001lem4  14710  4001prm  14711  sincos6thpi  23074  binom4  23378  quartlem1  23385  log2ublem3  23476  log2ub  23477  bclbnd  23753  4cycl4v4e  24868  4cycl4dv4e  24870  ex-opab  25355  ex-ind-dvds  25372  fib4  28607  fib5  28608  4bc3eq4  29352  bpoly4  30049  lhe4.4ex1a  31475  stoweidlem26  32047  stoweidlem34  32055  inductionexd  38419
  Copyright terms: Public domain W3C validator