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

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

Proof of Theorem inindir
StepHypRef Expression
1 inidm 4193 . . 3 (𝐶𝐶) = 𝐶
21ineq2i 4184 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐵) ∩ 𝐶)
3 in4 4200 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐶) ∩ (𝐵𝐶))
42, 3eqtr3i 2844 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∩ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530   ∩ cin 3933 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-in 3941 This theorem is referenced by:  difindir  4257  resindir  5863  predin  6164  restbas  21758  connsuba  22020  kgentopon  22138  trfbas2  22443  trfil2  22487  fclsrest  22624  trust  22830  chtdif  25727  ppidif  25732  mdslmd1lem1  30094  mdslmd1lem2  30095  mddmdin0i  30200  ballotlemgun  31770  cvmsss2  32509
 Copyright terms: Public domain W3C validator