diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index e19e4d577f9a78833ed0c2b3facd8467d9aeea8e..0b1a61b92bc6592ddf45a5e153f9556390375f00 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1689,6 +1689,13 @@ Global Instance exist_absorbing {A} (Φ : A → PROP) :
   (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
 Proof. rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono. Qed.
 
+Global Instance impl_absorbing P Q :
+  Persistent P → Absorbing P → Absorbing Q → Absorbing (P → Q).
+Proof.
+  intros. rewrite /Absorbing. apply impl_intro_l.
+  rewrite persistent_and_affinely_sep_l_1 absorbingly_sep_r.
+  by rewrite -persistent_and_affinely_sep_l impl_elim_r.
+Qed.
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
   Absorbing (x ≡ y : PROP)%I.
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.