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

Theorem 4p1e5 10658
Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
4p1e5  |-  ( 4  +  1 )  =  5

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 10593 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2467 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398  (class class class)co 6270   1c1 9482    + caddc 9484   4c4 10583   5c5 10584
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-5 10593
This theorem is referenced by:  8t7e56  11069  9t6e54  11075  s5len  12849  2exp6OLD  14657  2exp16  14659  prmlem2  14689  163prm  14694  317prm  14695  631prm  14696  1259lem1  14697  1259lem2  14698  1259lem3  14699  1259lem4  14700  2503lem1  14703  2503lem2  14704  2503lem3  14705  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  log2ublem3  23476  log2ub  23477  fib5  28608  fib6  28609  bpoly4  30049  5m4e1  33600
  Copyright terms: Public domain W3C validator