diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 0f25045e7acfdf3f1967e2a167dba87d5640a630..5a34be3273f20775ee548b7950bb908eb42def1f 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -253,6 +253,15 @@ 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_wp_step s E e P Φ :
+  TCEq (to_val e) None →
+  ▷ P -∗
+  WP e @ s; E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ s; E {{ Φ }}.
+Proof.
+  iIntros (?) "HP Hwp".
+  iApply (wp_step_fupd _ _ E _ P with "[HP]"); [auto..|]. by iApply twp_wp.
+Qed.
 End twp.
 
 (** Proofmode class instances *)