Theorem in4

Description: Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001)

	Ref	Expression
Assertion	in4	$$⊢\left(A\cap B\right)\cap \left(C\cap D\right)=\left(A\cap C\right)\cap \left(B\cap D\right)$$

Proof

Step	Hyp	Ref	Expression
1		in12	$$⊢B\cap \left(C\cap D\right)=C\cap \left(B\cap D\right)$$
2	1	ineq2i	$$⊢A\cap \left(B\cap \left(C\cap D\right)\right)=A\cap \left(C\cap \left(B\cap D\right)\right)$$
3		inass	$$⊢\left(A\cap B\right)\cap \left(C\cap D\right)=A\cap \left(B\cap \left(C\cap D\right)\right)$$
4		inass	$$⊢\left(A\cap C\right)\cap \left(B\cap D\right)=A\cap \left(C\cap \left(B\cap D\right)\right)$$
5	2 3 4	3eqtr4i	$$⊢\left(A\cap B\right)\cap \left(C\cap D\right)=\left(A\cap C\right)\cap \left(B\cap D\right)$$