diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 6278dc971dbcbdf978cf2e3ac32a194514af81c8..f2fd5b3e1c16549a92d1431335726e7283d1c18a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -257,6 +257,12 @@ Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
 Lemma twp_wand_r s E e Φ Ψ :
   WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
 Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+Lemma twp_frame_wand s E e Φ R :
+  R -∗ WP e @ s; E [{ v, R -∗ Φ v }] -∗ WP e @ s; E [{ Φ }].
+Proof.
+  iIntros "HR HWP". iApply (twp_wand with "HWP").
+  iIntros (v) "HΦ". by iApply "HΦ".
+Qed.
 
 Lemma twp_wp_step s E e P Φ :
   TCEq (to_val e) None →