Theorem inrot

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

	Ref	Expression
Assertion	inrot	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐶 ∩ 𝐴 ) ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		in31	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ 𝐴 )
2		in32	⊢ ( ( 𝐶 ∩ 𝐵 ) ∩ 𝐴 ) = ( ( 𝐶 ∩ 𝐴 ) ∩ 𝐵 )
3	1 2	eqtri	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐶 ∩ 𝐴 ) ∩ 𝐵 )