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

Metamath Proof Explorer

Theorem in31

Description: A rearrangement of intersection. (Contributed by NM, 27-Aug-2012)

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

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