![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inindir | Structured version Visualization version GIF version |
Description: Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.) |
Ref | Expression |
---|---|
inindir | ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inidm 4018 | . . 3 ⊢ (𝐶 ∩ 𝐶) = 𝐶 | |
2 | 1 | ineq2i 4009 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ 𝐶) |
3 | in4 4025 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | |
4 | 2, 3 | eqtr3i 2823 | 1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 ∩ cin 3768 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-in 3776 |
This theorem is referenced by: difindir 4083 resindir 5624 predin 5921 restbas 21291 connsuba 21552 kgentopon 21670 trfbas2 21975 trfil2 22019 fclsrest 22156 trust 22361 chtdif 25236 ppidif 25241 mdslmd1lem1 29709 mdslmd1lem2 29710 mddmdin0i 29815 ballotlemgun 31103 cvmsss2 31773 |
Copyright terms: Public domain | W3C validator |