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

Metamath Proof Explorer

Theorem in32

Description: A rearrangement of intersection. (Contributed by NM, 21-Apr-2001) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap B) \cap C = A \cap (B \cap C)$
2		in12	$⊢ A \cap (B \cap C) = B \cap (A \cap C)$
3		incom	$⊢ B \cap (A \cap C) = (A \cap C) \cap B$
4	1 2 3	3eqtri	$⊢ (A \cap B) \cap C = (A \cap C) \cap B$