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	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		inass	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )
2		in12	⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐵 ∩ ( 𝐴 ∩ 𝐶 ) )
3		incom	⊢ ( 𝐵 ∩ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐵 )
4	1 2 3	3eqtri	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∩ 𝐵 )