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

Theorem inindir 3400
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 3391 . . 3  |-  ( C  i^i  C )  =  C
21ineq2i 3380 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  B
)  i^i  C )
3 in4 3398 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  C
)  i^i  ( B  i^i  C ) )
42, 3eqtr3i 2318 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 1632    i^i cin 3164
This theorem is referenced by:  difindir  3437  resindir  4988  restbas  16905  consuba  17162  kgentopon  17249  trfbas2  17554  trfil2  17598  fclsrest  17735  chtdif  20412  ppidif  20417  mdslmd1lem1  22921  mdslmd1lem2  22922  mddmdin0i  23027  ballotlemgun  23099  cvmsss2  23820  predin  24260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator