diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 64c39eb32874fb9a3c1b7fa12a140ae3b207682d..70c554b24b27f6c90fb124293d3ca6991ce967e9 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -807,14 +807,16 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
   IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
-(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct] *)
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
   intros (φ'&->&?). rewrite /IntoExist (into_pure P).
   apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
-(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct] *)
 Global Instance into_exist_sep_pure P Q φ :
   IntoPureT P φ →
   TCOr (Affine P) (Absorbing Q) →
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 180eeee01dcc7ba69bbd0b8cee422b9fffafcadb..af6433bb866b587ba72d531ba052b0912e71a317 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1426,6 +1426,18 @@ Tactic Notation "iModCore" constr(H) :=
 
 (** [pat0] is the unparsed pattern, and is only used in error messages *)
 Local Ltac iDestructHypGo Hz pat0 pat :=
+  let iAndDestructAs pat1 pat2 :=
+      let Hy := iFresh in
+      iAndDestruct Hz as Hz Hy;
+      iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2 in
+  let iExistDestructPure gallina_id pat2 :=
+      lazymatch gallina_id with
+      | IGallinaAnon =>
+        iExistDestruct Hz as ? Hz; iDestructHypGo Hz pat0 pat2
+      | IGallinaNamed ?s =>
+        let x := string_to_ident s in
+        iExistDestruct Hz as x Hz; iDestructHypGo Hz pat0 pat2
+      end in
   lazymatch pat with
   | IFresh =>
      lazymatch Hz with
@@ -1444,9 +1456,11 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IList [[IDrop; ?pat2]] =>
      iAndDestructChoice Hz as Right Hz;
      iDestructHypGo Hz pat0 pat2
-  | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy;
-     iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
+  (* heuristic to fallback to [iAndDestruct] when both patterns are pure, since
+  the instances for [IntoAnd] are more general than for [IntoExist]. *)
+  | IList [[IPure ?id1; IPure ?id2]] => iAndDestructAs (IPure id1) (IPure id2)
+  | IList [[IPure ?gallina_id; ?pat2]] => iExistDestructPure gallina_id pat2
+  | IList [[?pat1; ?pat2]] => iAndDestructAs pat1 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
   | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9940220a322df3876e16151375d5b30367928fa0..0059095e0df1cf30bbdfee1b677feacd57616ce9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -251,6 +251,15 @@ Lemma test_iDestruct_exists_automatic_def P :
   an_exists P -∗ ∃ k, ▷^k P.
 Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
 
+(* use an Iris intro pattern [% H] to indicate iExistDestruct rather than (?) *)
+Lemma test_exists_intro_pattern_anonymous P (Φ: nat → PROP) :
+  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
+Proof.
+  iIntros "[HP1 [% HP2]]".
+  iExists y.
+  iFrame "HP1 HP2".
+Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
@@ -1379,6 +1388,14 @@ Proof.
   Fail iIntros "[H %H]".
 Abort.
 
+Lemma test_exists_intro_pattern P (Φ: nat → PROP) :
+  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
+Proof.
+  iIntros "[HP1 [%y HP2]]".
+  iExists y.
+  iFrame "HP1 HP2".
+Qed.
+
 End pure_name_tests.
 
 Section tactic_tests.