diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 1e6b323130699c911bdb281797410c9e5de53b74..ff23506f5590094cdc83f8f763c93e4328edec2c 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -215,9 +215,12 @@ Proof.
   rewrite {1}(persistent ⌜φ⌝%I) //.
 Qed.
 
-Global Instance from_pure_absorbingly P φ :
-  FromPure true P φ → FromPure false (<absorb> P) φ.
-Proof. rewrite /FromPure=> <- /=. by rewrite persistent_absorbingly_affinely. Qed.
+Global Instance from_pure_absorbingly P φ p :
+  FromPure true P φ → FromPure p (<absorb> P) φ.
+Proof.
+  rewrite /FromPure=> <- /=.
+  rewrite persistent_absorbingly_affinely affinely_if_elim //.
+Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
 Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 19c61a492d7859ef107847e1d224b2ccb0bd505f..bd5c516be1b7e553253a22010a2b312087d5b917 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -389,6 +389,10 @@ Qed.
 Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
 Proof. by iIntros (?). Qed.
 
+Lemma test_iPureIntro_absorbing (φ : Prop) :
+  φ → sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
+Proof. intros ?. iPureIntro. done. Qed.
+
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". auto. Qed.