Theorem iniin2

Description: Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	iniin2	$$⊢A\ne \varnothing \to B\cap \bigcap _{x\in A}C=\bigcap _{x\in A}\left(B\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		iinin2	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(B\cap C\right)=B\cap \bigcap _{x\in A}C$$
2	1	eqcomd	$$⊢A\ne \varnothing \to B\cap \bigcap _{x\in A}C=\bigcap _{x\in A}\left(B\cap C\right)$$