This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inindir

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

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

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