diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 01af4478a108554fc2cace5276ec5d95ee303f43..9af410500bda662d252057a7e22d3c48a46c549a 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1708,6 +1708,11 @@ Proof.
   intros HΦ HΨ c Hc. apply entails_eq_True, equiv_dist=>n.
   rewrite conv_compl. apply equiv_dist, entails_eq_True. done.
 Qed.
+Lemma limit_preserving_emp_valid {A : ofe} `{!Cofe A} (Φ : A → PROP) :
+  NonExpansive Φ → LimitPreserving (λ x, ⊢ Φ x).
+Proof.
+  intros. apply limit_preserving_entails; first solve_proper. done.
+Qed.
 Lemma limit_preserving_equiv {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
 Proof.