![]() |
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 4217 | . . 3 ⊢ (𝐶 ∩ 𝐶) = 𝐶 | |
2 | 1 | ineq2i 4207 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐵) ∩ 𝐶) |
3 | in4 4224 | . 2 ⊢ ((𝐴 ∩ 𝐵) ∩ (𝐶 ∩ 𝐶)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) | |
4 | 2, 3 | eqtr3i 2755 | 1 ⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∩ cin 3943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-in 3951 |
This theorem is referenced by: difindir 4281 resindir 6002 predin 6335 restbas 23106 connsuba 23368 kgentopon 23486 trfbas2 23791 trfil2 23835 fclsrest 23972 trust 24178 chtdif 27135 ppidif 27140 mdslmd1lem1 32207 mdslmd1lem2 32208 mddmdin0i 32313 ballotlemgun 34275 cvmsss2 35015 |
Copyright terms: Public domain | W3C validator |