Theorem inindir

Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		inidm	$$⊢C\cap C=C$$
2	1	ineq2i	$$⊢\left(A\cap B\right)\cap \left(C\cap C\right)=\left(A\cap B\right)\cap C$$
3		in4	$$⊢\left(A\cap B\right)\cap \left(C\cap C\right)=\left(A\cap C\right)\cap \left(B\cap C\right)$$
4	2 3	eqtr3i	$$⊢\left(A\cap B\right)\cap C=\left(A\cap C\right)\cap \left(B\cap C\right)$$