diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 29a89743969690eae98b773485853427c2cea3a6..e19e4d577f9a78833ed0c2b3facd8467d9aeea8e 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1339,6 +1339,13 @@ Proof.
   by rewrite -persistently_and_affinely_sep_l affinely_and_r affinely_and idemp.
 Qed.
 
+Lemma wand_impl_affinely_persistently P Q : (□ P -∗ Q) ⊣⊢ (bi_persistently P → Q).
+Proof.
+  apply (anti_symm (⊢)).
+  - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r.
+  - apply wand_intro_l. by rewrite -persistently_and_affinely_sep_l impl_elim_r.
+Qed.
+
 (* The combined affinely plainly modality *)
 Lemma affinely_plainly_elim P : ■ P ⊢ P.
 Proof. apply plainly_and_emp_elim. Qed.
@@ -1377,6 +1384,9 @@ Proof.
   by rewrite -plainly_and_affinely_sep_l affinely_and_r affinely_and idemp.
 Qed.
 
+Lemma wand_impl_affinely_plainly P Q : (■ P -∗ Q) ⊣⊢ (bi_plainly P → Q).
+Proof. by rewrite -(persistently_plainly P) wand_impl_affinely_persistently. Qed.
+
 (* Conditional affinely modality *)
 Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.