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

Theorem 4p1e5 10672
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 10607 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2480 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6294   1c1 9503    + caddc 9505   4c4 10597   5c5 10598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-5 10607
This theorem is referenced by:  8t7e56  11079  9t6e54  11085  s5len  12833  2exp6  14443  2exp16  14445  prmlem2  14475  163prm  14480  317prm  14481  631prm  14482  1259lem1  14483  1259lem2  14484  1259lem3  14485  1259lem4  14486  2503lem1  14489  2503lem2  14490  2503lem3  14491  4001lem1  14493  4001lem2  14494  4001lem3  14495  4001lem4  14496  log2ublem3  23122  log2ub  23123  fib5  28137  fib6  28138  bpoly4  29716  5m4e1  32586
  Copyright terms: Public domain W3C validator