diff --git a/CHANGELOG.md b/CHANGELOG.md
index f68ddcb9fd89ca83711a8c3f142e719228de58ec..d9019babc26e4932e519a3ac468771d64bf9b575 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -94,6 +94,8 @@ Coq 8.13 is no longer supported.
     `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
 * Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
   `-∗` and `∗-∗` connectives. (by Ike Mulder)
+* Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
+  can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index a5f5d62b307d37a701303d1f47e8b93bf65c7a0b..fe6d60b1d37ad8a69986ddde71d8525979aafd05 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -12,6 +12,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
 Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Global Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
+Notation "P ∗-∗ Q" := (⊢ P ∗-∗ Q) : stdpp_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Global Arguments Persistent {_} _%I : simpl never.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2326056adf078484872e36119cb1546877474276..7ebd11da3560c6f616c69d120a05cdbda8ed2b21 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -9,10 +9,14 @@ Section tests.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
-Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_emp_wand_iff P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
-Lemma test_eauto_isplit_biwand P : ⊢ P ∗-∗ P.
+Lemma test_eauto_iSplit_wand_iff P : ⊢ P ∗-∗ P.
+Proof. eauto. Qed.
+
+(** We get the [⊢] automatically from the notation in [stdpp_scope]. *)
+Lemma test_eauto_iSplit_wand_iff_std_scope P : P ∗-∗ P.
 Proof. eauto. Qed.
 
 Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝.