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

Theorem inindir 3519
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 3510 . . 3  |-  ( C  i^i  C )  =  C
21ineq2i 3499 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  B
)  i^i  C )
3 in4 3517 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  C
)  i^i  ( B  i^i  C ) )
42, 3eqtr3i 2426 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 3279
This theorem is referenced by:  difindir  3556  resindir  5122  restbas  17176  consuba  17436  kgentopon  17523  trfbas2  17828  trfil2  17872  fclsrest  18009  trust  18212  chtdif  20894  ppidif  20899  mdslmd1lem1  23781  mdslmd1lem2  23782  mddmdin0i  23887  ballotlemgun  24735  cvmsss2  24914  predin  25403
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287
  Copyright terms: Public domain W3C validator