diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index f0a8571482343154899b2385de7c379f3dd8ee83..7dde67cb76e95f78d11fbd7be7f12d77a4bae658 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1632,14 +1632,12 @@ would be its only field. *)
 Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
 Proof. rewrite intuitionistic_intuitionistically. done. Qed.
 
+Lemma intuitionistically_intro P Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.
+
 Section persistent_bi_absorbing.
   Context `{!BiAffine PROP}.
 
-  Lemma intuitionistically_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-  Proof.
-    intros HP. rewrite (persistent P) HP intuitionistically_into_persistently //.
-  Qed.
-
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
   Proof.