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

Theorem 4p1e5 10105
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 10061 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2440 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff set class
Syntax hints:    = wceq 1652  (class class class)co 6081   1c1 8991    + caddc 8993   4c4 10051   5c5 10052
This theorem is referenced by:  8t7e56  10475  9t6e54  10481  s5len  11857  2exp6  13422  2exp16  13424  prmlem2  13442  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  2503lem1  13456  2503lem2  13457  2503lem3  13458  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  log2ublem3  20788  log2ub  20789  bpoly4  26105  5m4e1  28535
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429  df-5 10061
  Copyright terms: Public domain W3C validator