Theorem indir 4226

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

Assertion

Ref	Expression
indir	⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

Proof of Theorem indir

Step	Hyp	Ref	Expression
1		indi 4224	. 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
2		incom 4149	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵))
3		incom 4149	. . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
4		incom 4149	. . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵)
5	3, 4	uneq12i 4106	. 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
6	1, 2, 5	3eqtr4i 2769	1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1542   ∪ cun 3887   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-in 3896

This theorem is referenced by:  difundir  4231  undisj1  4402  disjpr2  4657  resundir  5959  predun  6292  djuassen  10101  fin23lem26  10247  fpwwe2lem12  10565  neitr  23145  fiuncmp  23369  connsuba  23385  trfil2  23852  tsmsres  24109  trust  24194  restmetu  24535  volun  25512  uniioombllem3  25552  itgsplitioo  25805  ppiprm  27114  chtprm  27116  chtdif  27121  ppidif  27126  cycpmco2f1  33185  carsgclctunlem1  34461  ballotlemfp1  34636  ballotlemgun  34669  mrsubvrs  35704  mthmpps  35764  fixun  36089  mbfposadd  37988  iunrelexp0  44129  31prm  48060