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

Theorem 4p1e5 10998
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 10926 . 2 5 = (4 + 1)
21eqcomi 2615 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6524  1c1 9790   + caddc 9792  4c4 10916  5c5 10917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599  df-5 10926
This theorem is referenced by:  8t7e56  11490  9t6e54  11496  s5len  13438  bpoly4  14572  2exp16  15578  prmlem2  15608  163prm  15613  317prm  15614  631prm  15615  prmo5  15617  1259lem1  15619  1259lem2  15620  1259lem3  15621  1259lem4  15622  2503lem1  15625  2503lem2  15626  2503lem3  15627  4001lem1  15629  4001lem2  15630  4001lem3  15631  4001lem4  15632  log2ublem3  24389  log2ub  24390  ex-exp  26462  ex-fac  26463  fib5  29597  fib6  29598  fmtno1  39793  257prm  39813  fmtno4prmfac  39824  fmtno4nprmfac193  39826  fmtno5faclem2  39832  31prm  39852  127prm  39855  m11nprm  39858  nnsum3primesle9  40012  5m4e1  42312
  Copyright terms: Public domain W3C validator