Theorem inindir

Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		inidm	|- ( C i^i C ) = C
2	1	ineq2i	|- ( ( A i^i B ) i^i ( C i^i C ) ) = ( ( A i^i B ) i^i C )
3		in4	|- ( ( A i^i B ) i^i ( C i^i C ) ) = ( ( A i^i C ) i^i ( B i^i C ) )
4	2 3	eqtr3i	|- ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i ( B i^i C ) )