Theorem in12

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

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

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
2	1	ineq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝐵 ∩ 𝐴 ) ∩ 𝐶 )
3		inass	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )
4		inass	⊢ ( ( 𝐵 ∩ 𝐴 ) ∩ 𝐶 ) = ( 𝐵 ∩ ( 𝐴 ∩ 𝐶 ) )
5	2 3 4	3eqtr3i	⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐵 ∩ ( 𝐴 ∩ 𝐶 ) )