Theorem in4

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

	Ref	Expression
Assertion	in4	|- ( ( A i^i B ) i^i ( C i^i D ) ) = ( ( A i^i C ) i^i ( B i^i D ) )

Proof

Step	Hyp	Ref	Expression
1		in12	|- ( B i^i ( C i^i D ) ) = ( C i^i ( B i^i D ) )
2	1	ineq2i	|- ( A i^i ( B i^i ( C i^i D ) ) ) = ( A i^i ( C i^i ( B i^i D ) ) )
3		inass	|- ( ( A i^i B ) i^i ( C i^i D ) ) = ( A i^i ( B i^i ( C i^i D ) ) )
4		inass	|- ( ( A i^i C ) i^i ( B i^i D ) ) = ( A i^i ( C i^i ( B i^i D ) ) )
5	2 3 4	3eqtr4i	|- ( ( A i^i B ) i^i ( C i^i D ) ) = ( ( A i^i C ) i^i ( B i^i D ) )