Theorem indir 4276

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 4274	. 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
2		incom 4202	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵))
3		incom 4202	. . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
4		incom 4202	. . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵)
5	3, 4	uneq12i 4162	. 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
6	1, 2, 5	3eqtr4i 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1539   ∪ cun 3947   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3954  df-in 3956

This theorem is referenced by:  difundir  4281  undisj1  4462  disjpr2  4718  resundir  5997  predun  6330  djuassen  10177  fin23lem26  10324  fpwwe2lem12  10641  neitr  22906  fiuncmp  23130  connsuba  23146  trfil2  23613  tsmsres  23870  trust  23956  restmetu  24301  volun  25296  uniioombllem3  25336  itgsplitioo  25589  ppiprm  26889  chtprm  26891  chtdif  26896  ppidif  26901  cycpmco2f1  32551  carsgclctunlem1  33612  ballotlemfp1  33786  ballotlemgun  33819  mrsubvrs  34809  mthmpps  34869  fixun  35183  mbfposadd  36840  metakunt17  41309  metakunt21  41313  metakunt22  41314  metakunt24  41316  iunrelexp0  42757  31prm  46565