![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineqan12d | Structured version Visualization version GIF version |
Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.) |
Ref | Expression |
---|---|
ineq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
ineqan12d.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
ineqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | ineqan12d.2 | . 2 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | ineq12 4208 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2an 594 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-in 3954 |
This theorem is referenced by: funprg 6613 funtpg 6614 funcnvpr 6621 funcnvqp 6623 fvun1 6993 fndmin 7058 ofrfvalg 7698 offval 7699 offval3 7996 fpar 8130 offsplitfpar 8133 wfrlem4OLD 8342 fisn 9470 ixxin 13395 vdwmc 16980 fvcosymgeq 19427 cssincl 21684 inmbl 25562 iundisj2 25569 itg1addlem3 25718 fh1 31551 iundisj2f 32510 of0r 32596 iundisj2fi 32699 satffunlem1lem1 35230 satffunlem2lem1 35232 disjeccnvep 37982 disjecxrn 38087 br1cosscnvxrn 38172 |
Copyright terms: Public domain | W3C validator |