Theorem indir

Description: Distributive law for intersection over union. Theorem 28 of Suppes p. 27. (Contributed by NM, 30-Sep-2002)

	Ref	Expression
Assertion	indir	|- ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )

Proof

Step	Hyp	Ref	Expression
1		indi	|- ( C i^i ( A u. B ) ) = ( ( C i^i A ) u. ( C i^i B ) )
2		incom	|- ( ( A u. B ) i^i C ) = ( C i^i ( A u. B ) )
3		incom	|- ( A i^i C ) = ( C i^i A )
4		incom	|- ( B i^i C ) = ( C i^i B )
5	3 4	uneq12i	|- ( ( A i^i C ) u. ( B i^i C ) ) = ( ( C i^i A ) u. ( C i^i B ) )
6	1 2 5	3eqtr4i	|- ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )