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

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

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 9823 . 2
21eqcomi 2300 1
 Colors of variables: wff set class Syntax hints:   wceq 1632  (class class class)co 5874  c1 8754   caddc 8756  c4 9813  c5 9814 This theorem is referenced by:  8t7e56  10233  9t6e54  10239  s5len  11559  2exp6  13117  2exp16  13119  prmlem2  13137  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  2503lem1  13151  2503lem2  13152  2503lem3  13153  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  log2ublem3  20260  log2ub  20261  bpoly4  24866  5m4e1  28516 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-5 9823
 Copyright terms: Public domain W3C validator