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

Theorem 4p1e5 11031
 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 10959 . 2 5 = (4 + 1)
21eqcomi 2619 1 (4 + 1) = 5
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  4c4 10949  5c5 10950 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-5 10959 This theorem is referenced by:  8t7e56  11537  9t6e54  11543  s5len  13495  bpoly4  14629  2exp16  15635  prmlem2  15665  163prm  15670  317prm  15671  631prm  15672  prmo5  15674  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  2503lem1  15682  2503lem2  15683  2503lem3  15684  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  log2ublem3  24475  log2ub  24476  ex-exp  26699  ex-fac  26700  fib5  29794  fib6  29795  fmtno1  39991  257prm  40011  fmtno4prmfac  40022  fmtno4nprmfac193  40024  fmtno5faclem2  40030  31prm  40050  127prm  40053  m11nprm  40056  nnsum3primesle9  40210  5m4e1  42352
 Copyright terms: Public domain W3C validator