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

Theorem 4p1e5 11114
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 11042 . 2 5 = (4 + 1)
21eqcomi 2630 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6615  1c1 9897   + caddc 9899  4c4 11032  5c5 11033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-5 11042
This theorem is referenced by:  8t7e56  11621  9t6e54  11627  s5len  13597  bpoly4  14734  2exp16  15740  prmlem2  15770  163prm  15775  317prm  15776  631prm  15777  prmo5  15779  1259lem1  15781  1259lem2  15782  1259lem3  15783  1259lem4  15784  2503lem1  15787  2503lem2  15788  2503lem3  15789  4001lem1  15791  4001lem2  15792  4001lem3  15793  4001lem4  15794  log2ublem3  24609  log2ub  24610  ex-exp  27195  ex-fac  27196  fib5  30290  fib6  30291  fmtno1  40782  257prm  40802  fmtno4prmfac  40813  fmtno4nprmfac193  40815  fmtno5faclem2  40821  31prm  40841  127prm  40844  m11nprm  40847  nnsum3primesle9  41001  5m4e1  41876
  Copyright terms: Public domain W3C validator