Theorem in13

Description: A rearrangement of intersection. (Contributed by NM, 27-Aug-2012)

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

Proof

Step	Hyp	Ref	Expression
1		in32	|- ( ( B i^i C ) i^i A ) = ( ( B i^i A ) i^i C )
2		incom	|- ( A i^i ( B i^i C ) ) = ( ( B i^i C ) i^i A )
3		incom	|- ( C i^i ( B i^i A ) ) = ( ( B i^i A ) i^i C )
4	1 2 3	3eqtr4i	|- ( A i^i ( B i^i C ) ) = ( C i^i ( B i^i A ) )