Theorem inindir 4154

Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)

Assertion

Ref	Expression
inindir	⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))

Proof of Theorem inindir

Step	Hyp	Ref	Expression
1		inidm 4145	. . 3 ⊢ (𝐶 ∩ 𝐶) = 𝐶
2	1	ineq2i 4136	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ 𝐶)
3		in4 4152	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
4	2, 3	eqtr3i 2823	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1538   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888

This theorem is referenced by:  difindir  4209  resindir  5835  predin  6139  restbas  21763  connsuba  22025  kgentopon  22143  trfbas2  22448  trfil2  22492  fclsrest  22629  trust  22835  chtdif  25743  ppidif  25748  mdslmd1lem1  30108  mdslmd1lem2  30109  mddmdin0i  30214  ballotlemgun  31892  cvmsss2  32634