diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 55fb9ddbe6..b8e0bc5432 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -208,11 +208,6 @@ instance : LawfulBEq String := inferInstance
 
 /-! # Logical connectives and equality -/
 
-def implies (a b : Prop) := a → b
-
-theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
-  fun hp => h₂ (h₁ hp)
-
 def trivial : True := ⟨⟩
 
 theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=