Theorem in12

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

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

Proof

Step	Hyp	Ref	Expression
1		incom	|- ( A i^i B ) = ( B i^i A )
2	1	ineq1i	|- ( ( A i^i B ) i^i C ) = ( ( B i^i A ) i^i C )
3		inass	|- ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) )
4		inass	|- ( ( B i^i A ) i^i C ) = ( B i^i ( A i^i C ) )
5	2 3 4	3eqtr3i	|- ( A i^i ( B i^i C ) ) = ( B i^i ( A i^i C ) )