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

Theorem 4p1e5 11772
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 11692 . 2 5 = (4 + 1)
21eqcomi 2835 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7148  1c1 10527   + caddc 10529  4c4 11683  5c5 11684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-5 11692
This theorem is referenced by:  8t7e56  12207  9t6e54  12213  s5len  14252  bpoly4  15403  2exp16  16414  prmlem2  16443  163prm  16448  317prm  16449  631prm  16450  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  2503lem1  16460  2503lem2  16461  2503lem3  16462  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  log2ublem3  25440  log2ub  25441  ex-exp  28143  ex-fac  28144  fib5  31549  fib6  31550  hgt750lemd  31805  hgt750lem2  31809  3cubeslem3l  39148  3cubeslem3r  39149  fmtno1  43535  257prm  43555  fmtno4prmfac  43566  fmtno4nprmfac193  43568  fmtno5faclem2  43574  31prm  43592  127prm  43595  m11nprm  43598  2exp340mod341  43730  nnsum3primesle9  43791  5m4e1  44730
  Copyright terms: Public domain W3C validator