diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
index d42778a14..c4ee2d50b 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/api/Inference.scala
@@ -33,3 +33,21 @@ object Inference {
   ): Inference[P, C] =
     Inference(i1.isValid && i2.isValid, show.format(i1.show, i2.show))
 }
+
+/**
+ * Similar to `Inference[P, C]` but will not implicitly manifest if `C` cannot be
+ * inferred from `P`.
+ *
+ * It is intended to be used with chained implicit definitions that require proof that `P ==> C`
+ */
+case class Implies[P, C](show: String)
+
+object Implies {
+  import scala.reflect.macros.blackbox
+  import Inference.==>
+
+  def manifest[A: c.WeakTypeTag, B: c.WeakTypeTag](
+      c: blackbox.Context
+  )(ir: c.Expr[A ==> B]): c.Expr[Implies[A, B]] =
+    c.universe.reify(Implies[A, B]((ir.splice).show))
+}
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
index d1f8a2365..1f182d90b 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/auto.scala
@@ -1,6 +1,6 @@
 package eu.timepit.refined
 
-import eu.timepit.refined.api.{Refined, RefType, Validate}
+import eu.timepit.refined.api.{Implies, Refined, RefType, Validate}
 import eu.timepit.refined.api.Inference.==>
 import eu.timepit.refined.macros.{InferMacro, RefineMacro}
 import shapeless.tag.@@
@@ -32,6 +32,11 @@ object auto {
       ir: A ==> B
   ): F[T, B] = macro InferMacro.impl[F, T, A, B]
 
+  implicit def autoImply[A, B](
+      implicit
+      ir: A ==> B
+  ): Implies[A, B] = macro InferMacro.implies[A, B]
+
   /**
    * Implicitly unwraps the `T` from a value of type `F[T, P]` using the
    * `[[api.RefType]]` instance of `F`. This allows a `F[T, P]` to be
diff --git a/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala b/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
index 5b3615582..c604575b1 100644
--- a/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
+++ b/modules/core/shared/src/main/scala/eu/timepit/refined/macros/InferMacro.scala
@@ -1,5 +1,6 @@
 package eu.timepit.refined.macros
 
+import eu.timepit.refined.api.Implies
 import eu.timepit.refined.api.Inference.==>
 import eu.timepit.refined.api.RefType
 import eu.timepit.refined.internal.Resources
@@ -20,4 +21,12 @@ class InferMacro(val c: blackbox.Context) extends MacroUtils {
 
     refTypeInstance(rt).unsafeRewrapM(c)(ta)
   }
+
+  def implies[A: c.WeakTypeTag, B: c.WeakTypeTag](ir: c.Expr[A ==> B]): c.Expr[Implies[A, B]] = {
+    val inference = eval(ir)
+    if (inference.notValid) {
+      abort(Resources.invalidInference(weakTypeOf[A].toString, weakTypeOf[B].toString))
+    }
+    Implies.manifest(c)(ir)
+  }
 }
diff --git a/modules/core/shared/src/test/scala/eu/timepit/refined/AutoSpec.scala b/modules/core/shared/src/test/scala/eu/timepit/refined/AutoSpec.scala
index 5fec037ad..42acf7d66 100644
--- a/modules/core/shared/src/test/scala/eu/timepit/refined/AutoSpec.scala
+++ b/modules/core/shared/src/test/scala/eu/timepit/refined/AutoSpec.scala
@@ -1,9 +1,10 @@
 package eu.timepit.refined
 
-import eu.timepit.refined.api.Refined
+import eu.timepit.refined.api.{Implies, Refined}
 import eu.timepit.refined.auto._
 import eu.timepit.refined.char.{Digit, Letter}
 import eu.timepit.refined.generic._
+import eu.timepit.refined.numeric.{Greater}
 import eu.timepit.refined.types.numeric.PosInt
 import org.scalacheck.Prop._
 import org.scalacheck.Properties
@@ -22,6 +23,15 @@ class AutoSpec extends Properties("auto") {
     a == b
   }
 
+  property("autoImply") = secure {
+    val t = implicitly[Implies[Greater[W.`1`.T], Greater[W.`0`.T]]]
+    illTyped(
+      "implicitly[Implies[Greater[W.`-1`.T], Greater[W.`0`.T]]]",
+      """type mismatch \(invalid inference\):\s*eu.timepit.refined.numeric.Greater\[Int\(-1\)\] does not imply\s*eu.timepit.refined.numeric.Greater\[Int\(0\)\]"""
+    )
+    t.show == "greaterInference(1, 0)"
+  }
+
   property("autoUnwrap: PosInt: Int") = secure {
     val a: PosInt = PosInt.unsafeFrom(1)
     val b: Int = a