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

Theorem inindir 3387
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 3378 . . 3  |-  ( C  i^i  C )  =  C
21ineq2i 3367 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  B
)  i^i  C )
3 in4 3385 . 2  |-  ( ( A  i^i  B )  i^i  ( C  i^i  C ) )  =  ( ( A  i^i  C
)  i^i  ( B  i^i  C ) )
42, 3eqtr3i 2305 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 1623    i^i cin 3151
This theorem is referenced by:  difindir  3424  resindir  4972  restbas  16889  consuba  17146  kgentopon  17233  trfbas2  17538  trfil2  17582  fclsrest  17719  chtdif  20396  ppidif  20401  mdslmd1lem1  22905  mdslmd1lem2  22906  mddmdin0i  23011  ballotlemgun  23083  cvmsss2  23805  predin  24189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator