diff --git a/CHANGELOG.md b/CHANGELOG.md
index cd33b885352b49fd6cd69575593aa2b1d33623f3..e926aad99efc4141c103ad5bd532df24a14c6b03 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,7 @@ Coq 8.13 is no longer supported.
     particular, replace `apply` by `iApply`).
   - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
     between the old and new way of interpreting `P -∗ Q`.
+* Add `auto` hint to introduce the BI version of `↔`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 1434459a97d97cb04f8c826ca475a8882ec9b47e..b0ce4dcf09b57832864d2a3d4a75ace04d1a8ffa 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3511,6 +3511,7 @@ Global Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
 
 Global Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.
+Global Hint Extern 1 (envs_entails _ (_ ↔ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.
 Global Hint Extern 1 (envs_entails _ (â–· _)) => iNext : core.
 Global Hint Extern 1 (envs_entails _ (â–  _)) => iModIntro : core.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b235b26ebd17e244dc564fc274380ab636a432a3..5e06d6df43253007fbd4e493130f87a9ff6af086 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1405,6 +1405,11 @@ Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP
   □ P -∗ ∃ _ : nat, □ P.
 Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
 
+Lemma test_auto_iff P : ⊢ P ↔ P.
+Proof. auto. Qed.
+
+Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
+Proof. auto. Qed.
 End tests.
 
 Section parsing_tests.