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

Theorem 4p1e5 10669
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 10604 . 2  |-  5  =  ( 4  +  1 )
21eqcomi 2456 1  |-  ( 4  +  1 )  =  5
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281   1c1 9496    + caddc 9498   4c4 10594   5c5 10595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-5 10604
This theorem is referenced by:  8t7e56  11078  9t6e54  11084  s5len  12839  2exp6OLD  14554  2exp16  14556  prmlem2  14586  163prm  14591  317prm  14592  631prm  14593  1259lem1  14594  1259lem2  14595  1259lem3  14596  1259lem4  14597  2503lem1  14600  2503lem2  14601  2503lem3  14602  4001lem1  14604  4001lem2  14605  4001lem3  14606  4001lem4  14607  log2ublem3  23255  log2ub  23256  fib5  28321  fib6  28322  bpoly4  29796  5m4e1  32947
  Copyright terms: Public domain W3C validator