diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 9bb024d0fe..7e8caee103 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -177,13 +177,14 @@ MK_CONSTANT(not_fn,    name("not"));
 MK_CONSTANT(forall_fn, name("forall"));
 MK_CONSTANT(exists_fn, name("exists"));
 
-MK_CONSTANT(mp_fn,        name("MP"));
-MK_CONSTANT(discharge_fn, name("Discharge"));
-MK_CONSTANT(refl_fn,      name("Refl"));
-MK_CONSTANT(case_fn,      name("Case"));
-MK_CONSTANT(subst_fn,     name("Subst"));
-MK_CONSTANT(eta_fn,       name("Eta"));
-
+// Axioms
+MK_CONSTANT(mp_fn,          name("MP"));
+MK_CONSTANT(discharge_fn,   name("Discharge"));
+MK_CONSTANT(refl_fn,        name("Refl"));
+MK_CONSTANT(case_fn,        name("Case"));
+MK_CONSTANT(subst_fn,       name("Subst"));
+MK_CONSTANT(eta_fn,         name("Eta"));
+MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 
 void add_basic_theory(environment & env) {
     env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
@@ -237,5 +238,8 @@ void add_basic_theory(environment & env) {
 
     // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
     env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));
+
+    // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
+    env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
 }
 }
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 7507f4245a..4667e9a8fb 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -147,6 +147,12 @@ bool is_eta_fn(expr const & e);
 /** \brief (Axiom) A : Type u, B : A -> Type u, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */
 inline expr Eta(expr const & A, expr const & B, expr const & f) { return mk_app(mk_eta_fn(), A, B, f); }
 
+/** \brief Implies Anti-symmetry */
+expr mk_imp_antisym_fn();
+bool is_imp_antisym_fn(expr const & e);
+/** \brief (Axiom) a : Bool, b : Bool, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
+inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
+
 class environment;
 /** \brief Initialize the environment with basic builtin declarations and axioms */
 void add_basic_theory(environment & env);