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

Metamath Proof Explorer

Theorem in12

Description: A rearrangement of intersection. (Contributed by NM, 21-Apr-2001)

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

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