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

Metamath Proof Explorer

Theorem inrot

Description: Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012)

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

Step	Hyp	Ref	Expression
1		in31	$⊢ (A \cap B) \cap C = (C \cap B) \cap A$
2		in32	$⊢ (C \cap B) \cap A = (C \cap A) \cap B$
3	1 2	eqtri	$⊢ (A \cap B) \cap C = (C \cap A) \cap B$