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

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

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 10622 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  4c4 10612  5c5 10613
This theorem is referenced by:  8t7e56  11097  9t6e54  11103  s5len  12858  2exp6OLD  14573  2exp16  14575  prmlem2  14605  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  2503lem1  14619  2503lem2  14620  2503lem3  14621  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  log2ublem3  23279  log2ub  23280  fib5  28344  fib6  28345  bpoly4  29821  5m4e1  33212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-5 10622
  Copyright terms: Public domain W3C validator