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

Theorem 4p1e5 9849
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 9807 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2287 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   4c4 9797   5c5 9798
This theorem is referenced by:  8t7e56  10217  9t6e54  10223  s5len  11543  2exp6  13101  2exp16  13103  prmlem2  13121  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  2503lem1  13135  2503lem2  13136  2503lem3  13137  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  log2ublem3  20244  log2ub  20245  bpoly4  24794  5m4e1  28259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-5 9807
  Copyright terms: Public domain W3C validator