diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 23fd37412855b1fd2e8d9cf7ee8709e95deb8f35..e202bc38259a2c857cf2c034028ebb9425b2b7ff 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -48,6 +48,9 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
+
 Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
 Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5208ff9e746132b7973b646ce32854d73988de2d..59d960c0c29e26091a1e01ccded83ab8c3dbb467 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -80,6 +80,9 @@ Qed.
 Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
 Proof. iIntros "H1 H2". by iFrame. Qed.
 
+Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
+Proof. iIntros (??) "H". auto. Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.