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

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

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 10061 . 2
21eqcomi 2440 1
 Colors of variables: wff set class Syntax hints:   wceq 1652  (class class class)co 6081  c1 8991   caddc 8993  c4 10051  c5 10052 This theorem is referenced by:  8t7e56  10475  9t6e54  10481  s5len  11857  2exp6  13422  2exp16  13424  prmlem2  13442  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  2503lem1  13456  2503lem2  13457  2503lem3  13458  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  log2ublem3  20788  log2ub  20789  bpoly4  26105  5m4e1  28535 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-cleq 2429  df-5 10061
 Copyright terms: Public domain W3C validator