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

Theorem 4p1e5 11424
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 11338 . 2 5 = (4 + 1)
21eqcomi 2774 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  (class class class)co 6842  1c1 10190   + caddc 10192  4c4 11329  5c5 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-5 11338
This theorem is referenced by:  8t7e56  11861  9t6e54  11867  s5len  13931  bpoly4  15074  2exp16  16073  prmlem2  16102  163prm  16107  317prm  16108  631prm  16109  prmo5  16111  1259lem1  16113  1259lem2  16114  1259lem3  16115  1259lem4  16116  2503lem1  16119  2503lem2  16120  2503lem3  16121  4001lem1  16123  4001lem2  16124  4001lem3  16125  4001lem4  16126  log2ublem3  24966  log2ub  24967  ex-exp  27701  ex-fac  27702  fib5  30850  fib6  30851  hgt750lemd  31109  hgt750lem2  31113  fmtno1  42061  257prm  42081  fmtno4prmfac  42092  fmtno4nprmfac193  42094  fmtno5faclem2  42100  31prm  42120  127prm  42123  m11nprm  42126  nnsum3primesle9  42290  5m4e1  43147
  Copyright terms: Public domain W3C validator