MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inindir Structured version   Visualization version   GIF version

Theorem inindir 4188
Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
inindir ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∩ (𝐵𝐶))

Proof of Theorem inindir
StepHypRef Expression
1 inidm 4179 . . 3 (𝐶𝐶) = 𝐶
21ineq2i 4170 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐵) ∩ 𝐶)
3 in4 4186 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐶) ∩ (𝐵𝐶))
42, 3eqtr3i 2767 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cin 3910
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-in 3918
This theorem is referenced by:  difindir  4243  resindir  5955  predin  6282  restbas  22512  connsuba  22774  kgentopon  22892  trfbas2  23197  trfil2  23241  fclsrest  23378  trust  23584  chtdif  26510  ppidif  26515  mdslmd1lem1  31270  mdslmd1lem2  31271  mddmdin0i  31376  ballotlemgun  33127  cvmsss2  33871
  Copyright terms: Public domain W3C validator