diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index e1e93317e3141335110f5f980bfefd8ee4254eb2..72ba65760aec43cc51a614be2551e794df820a27 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -449,6 +449,10 @@ Proof. rewrite /bi_affinely; apply _. Qed.
 Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
 Proof. rewrite /bi_absorbingly; apply _. Qed.
 
+Global Instance intuitionistically_timeless P :
+  Timeless (PROP:=PROP) emp → Timeless P → Timeless (□ P).
+Proof. rewrite /bi_intuitionistically; apply _. Qed.
+
 Global Instance eq_timeless {A : ofeT} (a b : A) :
   Discrete a → Timeless (PROP:=PROP) (a ≡ b).
 Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.