diff -r 48af00f6f110 -r 817d33f8aa7f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 05 14:32:50 2024 +0000
@@ -1089,6 +1089,8 @@
 
 lemma ex_disj_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" by iprover
 lemma all_conj_distrib: "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" by iprover
+lemma all_imp_conj_distrib: "(\<forall>x. P x \<longrightarrow> Q x \<and> R x) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<and> (\<forall>x. P x \<longrightarrow> R x)"
+  by iprover
 
 text \<open>
   \<^medskip> The \<open>\<and>\<close> congruence rule: not included by default!