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

Theorem 4p1e5 9865
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 9823 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2300 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   4c4 9813   5c5 9814
This theorem is referenced by:  8t7e56  10233  9t6e54  10239  s5len  11559  2exp6  13117  2exp16  13119  prmlem2  13137  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  2503lem1  13151  2503lem2  13152  2503lem3  13153  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  log2ublem3  20260  log2ub  20261  bpoly4  24866  5m4e1  28516
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-5 9823
  Copyright terms: Public domain W3C validator