src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sun Nov 07 23:35:11 2021 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 08 19:56:15 2021 +0100
@@ -1678,6 +1678,9 @@
 
 subsection \<open>Other simple lemmas and lemma duplicates\<close>
 
+lemma eq_iff_swap: "(x = y \<longleftrightarrow> P) \<Longrightarrow> (y = x \<longleftrightarrow> P)"
+by blast
+
 lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)"
   by auto