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

Theorem 4p1e5 11356
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 11284 . 2 5 = (4 + 1)
21eqcomi 2780 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  (class class class)co 6793  1c1 10139   + caddc 10141  4c4 11274  5c5 11275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-5 11284
This theorem is referenced by:  8t7e56  11862  9t6e54  11868  s5len  13854  bpoly4  14996  2exp16  16004  prmlem2  16034  163prm  16039  317prm  16040  631prm  16041  prmo5  16043  1259lem1  16045  1259lem2  16046  1259lem3  16047  1259lem4  16048  2503lem1  16051  2503lem2  16052  2503lem3  16053  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001lem4  16058  log2ublem3  24896  log2ub  24897  ex-exp  27649  ex-fac  27650  fib5  30807  fib6  30808  hgt750lemd  31066  hgt750lem2  31070  fmtno1  41981  257prm  42001  fmtno4prmfac  42012  fmtno4nprmfac193  42014  fmtno5faclem2  42020  31prm  42040  127prm  42043  m11nprm  42046  nnsum3primesle9  42210  5m4e1  43074
  Copyright terms: Public domain W3C validator