diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index d3f82d3ebf3f46c9886e188cc5a97a3281bd8d15..017795a34dc3c974ce8d2b5b1c03538d746e7890 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -161,7 +161,16 @@ Section inv.
     iIntros "!> [HP HQ]". by iApply "HcloseQ".
   Qed.
 
+  Lemma except_0_inv N P : ◇ inv N P ⊢ inv N P.
+  Proof.
+    rewrite inv_unseal /inv_def. iIntros "#H !>" (E ?).
+    iMod "H". by iApply "H".
+  Qed.
+
   (** ** Proof mode integration *)
+  Global Instance is_except_0_inv N P : IsExcept0 (inv N P).
+  Proof. apply except_0_inv. Qed.
+
   Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
 
   Global Instance into_acc_inv N P E: