diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6e1fa3f3e0aa9e9b3ca86f4cdd04c507ad9e9d9d..6dd3439030f094624e4174c86d85b2e958a84927 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,12 @@ lemma.
 * Add a construction `bi_tc` to create transitive closures of
   PROP-level binary relations.
 
+**Changes in `proofmode`:**
+
+* The proof mode introduction patterns "<-" and "->" are considered
+  intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
+  not dispose of hypotheses to perform the rewrite.
+
 ## Iris 4.0.0 (2022-08-18)
 
 The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 0ad6ea222e4769db22b6f630adad48e92aace582..aa3c6441747d4f605e081706129356b9f51d9c65 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -162,11 +162,11 @@ Elimination of logical connectives
     spatial context matching pattern `pat`.
 
   In case all branches of `ipat` start with a `#` (which causes the hypothesis
-  to be moved to the intuitionistic context) or with an `%` (which causes the
-  hypothesis to be moved to the pure Coq context), then one can use all
-  hypotheses for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal. Note that in this case the hypotheses still need to be
-  subdivided among the spatial premises.
+  to be moved to the intuitionistic context), with an `%` (which causes the
+  hypothesis to be moved to the pure Coq context), or with an `->`/`<-` (which
+  performs a rewrite), then one can use all hypotheses for proving the premises
+  of `pm_trm`, as well as for proving the resulting goal. Note that in this case
+  the hypotheses still need to be subdivided among the spatial premises.
 
 Separation logic-specific tactics
 ---------------------------------
diff --git a/iris/proofmode/intro_patterns.v b/iris/proofmode/intro_patterns.v
index b111915492176140c332e007c2badbc21798fe3b..1291f1b4bddd7d478534e0f700071f2b09b0c7f9 100644
--- a/iris/proofmode/intro_patterns.v
+++ b/iris/proofmode/intro_patterns.v
@@ -168,6 +168,7 @@ End intro_pat.
 Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
   match p with
   | IPure _ => true
+  | IRewrite _ => true
   | IIntuitionistic _ => true
   | IList pps => forallb (forallb intro_pat_intuitionistic) pps
   | ISimpl => true
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 700bb4382f4f29d49b28d6db96acfec96952bfc7..f53125f6efa65ddb17ec6c79a7df40e12165b99e 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -870,6 +870,15 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
+Lemma test_iDestruct_rewrite_not_consume P (x1 x2 : nat) :
+  (P -∗ ⌜ x1 = x2 ⌝) →
+  P -∗ ⌜ x1 = x2 ⌝ ∗ P.
+Proof.
+  iIntros (lemma) "HP". iDestruct (lemma with "HP") as "->".
+  auto. (* Make sure that "HP" has not been consumed; [auto] would fail
+  otherwise. *)
+Qed.
+
 Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.