Theorem indir 4275

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 4273	. 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
2		incom 4201	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵))
3		incom 4201	. . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴)
4		incom 4201	. . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵)
5	3, 4	uneq12i 4161	. 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵))
6	1, 2, 5	3eqtr4i 2771	1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1542   ∪ cun 3946   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3953  df-in 3955

This theorem is referenced by:  difundir  4280  undisj1  4461  disjpr2  4717  resundir  5995  predun  6327  djuassen  10170  fin23lem26  10317  fpwwe2lem12  10634  neitr  22676  fiuncmp  22900  connsuba  22916  trfil2  23383  tsmsres  23640  trust  23726  restmetu  24071  volun  25054  uniioombllem3  25094  itgsplitioo  25347  ppiprm  26645  chtprm  26647  chtdif  26652  ppidif  26657  cycpmco2f1  32271  carsgclctunlem1  33305  ballotlemfp1  33479  ballotlemgun  33512  mrsubvrs  34502  mthmpps  34562  fixun  34870  mbfposadd  36524  metakunt17  40990  metakunt21  40994  metakunt22  40995  metakunt24  40997  iunrelexp0  42439  31prm  46252