Theorem inindir 4189

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 4180	. . 3 ⊢ (𝐶 ∩ 𝐶) = 𝐶
2	1	ineq2i 4171	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ 𝐶)
3		in4 4187	. 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))
4	2, 3	eqtr3i 2789	1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1562   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913

This theorem is referenced by:  difindir  4247  resindir  5984  predin  6316  restbas  23220  connsuba  23482  kgentopon  23600  trfbas2  23905  trfil2  23949  fclsrest  24086  trust  24291  chtdif  27224  ppidif  27229  mdslmd1lem1  32530  mdslmd1lem2  32531  mddmdin0i  32636  ballotlemgun  34824  cvmsss2  35629