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

Theorem inindir 3503
Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
inindir  |-  ( ( A  i^i  B )  i^i  C )  =  ( ( A  i^i  C )  i^i  ( B  i^i  C ) )

Proof of Theorem inindir
StepHypRef Expression
1 inidm 3494 . . 3  |-  ( C  i^i  C )  =  C
21ineq2i 3483 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  B
)  i^i  C )
3 in4 3501 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  C
)  i^i  ( B  i^i  C ) )
42, 3eqtr3i 2410 1  |-  ( ( A  i^i  B )  i^i  C )  =  ( ( A  i^i  C )  i^i  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1649    i^i cin 3263
This theorem is referenced by:  difindir  3540  resindir  5104  restbas  17145  consuba  17405  kgentopon  17492  trfbas2  17797  trfil2  17841  fclsrest  17978  trust  18181  chtdif  20809  ppidif  20814  mdslmd1lem1  23677  mdslmd1lem2  23678  mddmdin0i  23783  ballotlemgun  24562  cvmsss2  24741  predin  25214
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-in 3271
  Copyright terms: Public domain W3C validator