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

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

Proof of Theorem inindir
StepHypRef Expression
1 inidm 4227 . . 3 (𝐶𝐶) = 𝐶
21ineq2i 4217 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐵) ∩ 𝐶)
3 in4 4234 . 2 ((𝐴𝐵) ∩ (𝐶𝐶)) = ((𝐴𝐶) ∩ (𝐵𝐶))
42, 3eqtr3i 2767 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958
This theorem is referenced by:  difindir  4293  resindir  6014  predin  6348  restbas  23166  connsuba  23428  kgentopon  23546  trfbas2  23851  trfil2  23895  fclsrest  24032  trust  24238  chtdif  27201  ppidif  27206  mdslmd1lem1  32344  mdslmd1lem2  32345  mddmdin0i  32450  ballotlemgun  34527  cvmsss2  35279
  Copyright terms: Public domain W3C validator