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 2769	1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-un 3953  df-in 3955

This theorem is referenced by:  difundir  4280  undisj1  4461  disjpr2  4717  resundir  5996  predun  6329  djuassen  10179  fin23lem26  10326  fpwwe2lem12  10643  neitr  23004  fiuncmp  23228  connsuba  23244  trfil2  23711  tsmsres  23968  trust  24054  restmetu  24399  volun  25394  uniioombllem3  25434  itgsplitioo  25687  ppiprm  26996  chtprm  26998  chtdif  27003  ppidif  27008  cycpmco2f1  32719  carsgclctunlem1  33780  ballotlemfp1  33954  ballotlemgun  33987  mrsubvrs  34977  mthmpps  35037  fixun  35351  mbfposadd  36999  metakunt17  41468  metakunt21  41472  metakunt22  41473  metakunt24  41475  iunrelexp0  42916  31prm  46724