diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index b076e5b792915ebb81b41f4a735ab1bf6b8e8a2f..944b2118dbf1feb25c50d3eb64694f09cbefa083 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -333,9 +333,13 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
 
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
-  eapply tac_and_split;
-    [let P := match goal with |- AndSplit ?P _ _ => P end in
-     apply _ || fail "iSplit:" P "not a conjunction"| |].
+  lazymatch goal with
+  | |- _ ⊢ _ =>
+    eapply tac_and_split;
+      [let P := match goal with |- AndSplit ?P _ _ => P end in
+       apply _ || fail "iSplit:" P "not a conjunction"| |]
+  | |- _ ⊣⊢ _ => apply (anti_symm (⊢))
+  end.
 
 Tactic Notation "iSplitL" constr(Hs) :=
   let Hs := words Hs in