diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index d9aa44e9c918a159b2af9ae44aec4983e2faeec7..8e6b4e1b8042a29edf1a383aaa6a2d1baee02794 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -197,6 +197,13 @@ Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
 Lemma later_absorbingly P : ▷ <absorb> P ⊣⊢ <absorb> ▷ P.
 Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
+Lemma later_affinely `{!BiAffine PROP} P : ▷ <affine> P ⊣⊢ <affine> ▷ P.
+Proof. by rewrite !affine_affinely. Qed.
+Lemma later_intuitionistically `{!BiAffine PROP} P : ▷ □ P ⊣⊢ □ ▷ P.
+Proof. by rewrite !intuitionistically_into_persistently later_persistently. Qed.
+Lemma later_intuitionistically_if `{!BiAffine PROP} p P : ▷ □?p P ⊣⊢ □?p ▷ P.
+Proof. destruct p; simpl; auto using later_intuitionistically. Qed.
+
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).