diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 8ce55d3ab6396ddb62c246d6900e7f4821c80273..724ffb34ae11b373ac8cb6e1fbf77a669bd83f16 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1398,6 +1398,8 @@ Global Instance affinely_if_affine p P : Affine P → Affine (<affine>?p P).
 Proof. destruct p; simpl; apply _. Qed.
 Global Instance intuitionistically_affine P : Affine (â–¡ P).
 Proof. rewrite /bi_intuitionistically. apply _. Qed.
+Global Instance intuitionistically_if_affine p P : Affine P → Affine (□?p P).
+Proof. destruct p; simpl; apply _. Qed.
 
 (* Absorbing instances *)
 Global Instance pure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.