Theorem in4

Description: Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001)

	Ref	Expression
Assertion	in4	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐶 ∩ 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		in12	⊢ ( 𝐵 ∩ ( 𝐶 ∩ 𝐷 ) ) = ( 𝐶 ∩ ( 𝐵 ∩ 𝐷 ) )
2	1	ineq2i	⊢ ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐶 ∩ 𝐷 ) ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵 ∩ 𝐷 ) ) )
3		inass	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐶 ∩ 𝐷 ) ) = ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐶 ∩ 𝐷 ) ) )
4		inass	⊢ ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐷 ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵 ∩ 𝐷 ) ) )
5	2 3 4	3eqtr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐶 ∩ 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐷 ) )