Theorem undir

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

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

Proof

Step	Hyp	Ref	Expression
1		undi	|- ( C u. ( A i^i B ) ) = ( ( C u. A ) i^i ( C u. B ) )
2		uncom	|- ( ( A i^i B ) u. C ) = ( C u. ( A i^i B ) )
3		uncom	|- ( A u. C ) = ( C u. A )
4		uncom	|- ( B u. C ) = ( C u. B )
5	3 4	ineq12i	|- ( ( A u. C ) i^i ( B u. C ) ) = ( ( C u. A ) i^i ( C u. B ) )
6	1 2 5	3eqtr4i	|- ( ( A i^i B ) u. C ) = ( ( A u. C ) i^i ( B u. C ) )