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

Theorem 4p1e5 10586
Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
4p1e5

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 10521 . 2
21eqcomi 2467 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370  (class class class)co 6222  1c1 9420   caddc 9422  4c4 10511  5c5 10512
This theorem is referenced by:  8t7e56  10987  9t6e54  10993  s5len  12678  2exp6  14273  2exp16  14275  prmlem2  14305  163prm  14310  317prm  14311  631prm  14312  1259lem1  14313  1259lem2  14314  1259lem3  14315  1259lem4  14316  2503lem1  14319  2503lem2  14320  2503lem3  14321  4001lem1  14323  4001lem2  14324  4001lem3  14325  4001lem4  14326  log2ublem3  22743  log2ub  22744  fib5  27244  fib6  27245  bpoly4  28658  5m4e1  31992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-5 10521
  Copyright terms: Public domain W3C validator