This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \cap B) \cup C = (A \cup C) \cap (B \cup C)$

Step	Hyp	Ref	Expression
1		undi	$⊢ C \cup (A \cap B) = (C \cup A) \cap (C \cup B)$
2		uncom	$⊢ (A \cap B) \cup C = C \cup (A \cap B)$
3		uncom	$⊢ A \cup C = C \cup A$
4		uncom	$⊢ B \cup C = C \cup B$
5	3 4	ineq12i	$⊢ (A \cup C) \cap (B \cup C) = (C \cup A) \cap (C \cup B)$
6	1 2 5	3eqtr4i	$⊢ (A \cap B) \cup C = (A \cup C) \cap (B \cup C)$