diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 40641c9b975a54c79f0e2b5c1fe7298add4d6ff9..2a1bbc10712a197b65dbe99ec5c7ae5c02bd2e93 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1094,6 +1094,9 @@ Proof.
     apply sep_mono; first done. apply and_elim_r.
 Qed.
 
+Lemma intuitionistically_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q).
+Proof. by rewrite /bi_intuitionistically persistently_impl_wand_2. Qed.
+
 Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
 Proof.
   apply (anti_symm (⊢)).