diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index e9fa2cacbada3722e313f4f27c01d1d82dadc2b3..3afa3312d65f28046c524f10e99bf8b671b30392 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -486,8 +486,6 @@ Proof.
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
-    intros P. unseal; split=> n  x ?? /=. by rewrite -(core_id_core ε).
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 0c7b86bd9798d8df7785d9c714781ae6a3349f17..4e8803833affce707c4b92518755583c0cc054b0 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -957,8 +957,11 @@ Proof.
 Qed.
 Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P.
 Proof.
-  apply (anti_symm _); first apply plainly_persistently_1.
-  by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
+  apply (anti_symm _).
+  - rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I).
+    rewrite -{2}(persistently_and_emp_elim P).
+    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
+  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
 Qed.
 
 Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 227fc6c29cd98b010b89a46d34acdca9a80a02fe..72e484cd7ccab411ccd762200b6bc2f69b80312b 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -129,8 +129,6 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P :
       bi_persistently P ⊢ bi_persistently (bi_persistently P);
-    bi_mixin_plainly_persistently_1 P :
-      bi_plainly (bi_persistently P) ⊢ bi_plainly P;
 
     (* In the ordered RA model [P ⊢ persisently emp] (which can currently still
     be derived from the plainly axioms, which will be removed): `ε ≼ core x` *)
@@ -453,9 +451,6 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P :
   bi_persistently P ⊢ bi_persistently (bi_persistently P).
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
-Lemma plainly_persistently_1 P :
-  bi_plainly (bi_persistently P) ⊢ bi_plainly P.
-Proof. eapply (bi_mixin_plainly_persistently_1 bi_entails), bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 1c216f2bcf6a28a7b279af66bbca4d7fcb28210b..c7bedbc1965f4d4140ae97e71285b0c79c7c169b 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -326,7 +326,6 @@ Proof.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
-  - intros P. split=> i /=. by setoid_rewrite bi.plainly_persistently_1.
   - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.