diff --git a/CHANGELOG.md b/CHANGELOG.md
index bb930d505340b8fc501bfe79ec0d40d8a6206a97..d392df165c6d743c5284ffb2eb807c9871dca374 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported.
 * Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2`
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
   `map_to_list`. (by Dorian Lesbre).
+- Make `persistently_True` a bi-entailment.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 7dde67cb76e95f78d11fbd7be7f12d77a4bae658..01af4478a108554fc2cace5276ec5d95ee303f43 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -951,8 +951,11 @@ Qed.
 
 Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
-Lemma persistently_True : True ⊢ <pers> True.
-Proof. rewrite persistently_True_emp. apply persistently_emp_intro. Qed.
+Lemma persistently_True : <pers> True ⊣⊢ True.
+Proof.
+  apply (anti_symm _); auto.
+  rewrite persistently_True_emp. apply persistently_emp_intro.
+Qed.
 
 Lemma persistently_and_emp P : <pers> P ⊣⊢ <pers> (emp ∧ P).
 Proof.
@@ -1005,7 +1008,7 @@ Lemma persistently_pure φ : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _).
   { by rewrite persistently_into_absorbingly absorbingly_pure. }
-  apply pure_elim'=> Hφ. rewrite persistently_True.
+  apply pure_elim'=> Hφ. rewrite -persistently_True.
   auto using persistently_mono, pure_intro.
 Qed.
 
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 4895c6b2788c8d0441e243d5408950104e37d2e8..06b7f5690b237b6d4646c9b8709273676a83ea01 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -657,13 +657,13 @@ once support for Coq < 8.15 is dropped *)
 
 Global Instance combine_seps_as_gives_nil : @CombineSepsAsGives PROP [] emp True.
 Proof.
-  split; first done. rewrite -persistently_True.
+  split; first done. rewrite persistently_True.
   by apply pure_intro.
 Qed.
 Global Instance combine_seps_as_gives_singleton P :
   CombineSepsAsGives [P] P True | 1.
 Proof.
-  split; first by rewrite /= right_id. rewrite -persistently_True.
+  split; first by rewrite /= right_id. rewrite persistently_True.
   by apply pure_intro.
 Qed.
 Global Instance combine_seps_gives_cons P Ps Q R Q' progress R' R'':
@@ -723,7 +723,7 @@ Global Instance combine_seps_as_from_as_gives Ps Q R :
   CombineSepsAs Ps Q.
 Proof.
   move => HPsQ. apply HPsQ. move => P P'. rewrite /CombineSepGives.
-  rewrite -persistently_True. by apply pure_intro.
+  rewrite persistently_True. by apply pure_intro.
 Qed.
 
 Lemma tac_combine_as Δ1 Δ2 Δ3 js p Ps j P Q :
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index b728ad51dd64b1df094ef99558bf48ad23ac38b6..46a92dbdc1785fafe7e7e1ce1941ad9855ffb930 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -398,7 +398,8 @@ Proof.
   rewrite /of_envs'. f_equiv.
   rewrite -persistent_and_affinely_sep_l. f_equiv.
   clear. induction Γp as [|Γp IH ? Q]; simpl.
-  { apply (anti_symm (⊢)); last by apply True_intro. apply persistently_True. }
+  { apply (anti_symm (⊢)); last by apply True_intro.
+    by rewrite persistently_True. }
   rewrite IH persistently_and. done.
 Qed.
 Lemma of_envs_alt Δ :