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

Theorem 3p1e4 10686
Description: 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
3p1e4

Proof of Theorem 3p1e4
StepHypRef Expression
1 df-4 10621 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  3c3 10611  4c4 10612
This theorem is referenced by:  7t6e42  11090  8t5e40  11095  9t5e45  11102  fac4  12361  hash4  12472  s4len  12857  2exp16  14575  43prm  14607  83prm  14608  317prm  14611  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  2503lem1  14619  2503lem2  14620  4001lem1  14623  4001lem2  14624  4001lem4  14626  4001prm  14627  sincos6thpi  22908  binom4  23181  quartlem1  23188  log2ublem3  23279  log2ub  23280  bclbnd  23555  4cycl4v4e  24666  4cycl4dv4e  24668  ex-opab  25153  ex-ind-dvds  25170  fib4  28343  fib5  28344  4bc3eq4  29111  bpoly4  29821  lhe4.4ex1a  31234  stoweidlem26  31808  stoweidlem34  31816  inductionexd  37967
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-4 10621
  Copyright terms: Public domain W3C validator