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

Theorem 4p1e5 10563
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 10498 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2467 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370  (class class class)co 6203   1c1 9398    + caddc 9400   4c4 10488   5c5 10489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-5 10498
This theorem is referenced by:  8t7e56  10963  9t6e54  10969  s5len  12642  2exp6  14237  2exp16  14239  prmlem2  14269  163prm  14274  317prm  14275  631prm  14276  1259lem1  14277  1259lem2  14278  1259lem3  14279  1259lem4  14280  2503lem1  14283  2503lem2  14284  2503lem3  14285  4001lem1  14287  4001lem2  14288  4001lem3  14289  4001lem4  14290  log2ublem3  22486  log2ub  22487  fib5  26955  fib6  26956  bpoly4  28369  5m4e1  31504
  Copyright terms: Public domain W3C validator