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

Metamath Proof Explorer

Theorem inin

Description: Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016)

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

Step	Hyp	Ref	Expression
1		in13	$⊢ A \cap (A \cap B) = B \cap (A \cap A)$
2		inidm	$⊢ A \cap A = A$
3	2	ineq2i	$⊢ B \cap (A \cap A) = B \cap A$
4		incom	$⊢ B \cap A = A \cap B$
5	1 3 4	3eqtri	$⊢ A \cap (A \cap B) = A \cap B$