| 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 4215 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
| 4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-in 3958 |
| This theorem is referenced by: funprg 6620 funtpg 6621 funcnvpr 6628 funcnvqp 6630 fvun1 7000 fndmin 7065 ofrfvalg 7705 offval 7706 offval3 8007 fpar 8141 offsplitfpar 8144 wfrlem4OLD 8352 fisn 9467 ixxin 13404 vdwmc 17016 fvcosymgeq 19447 cssincl 21706 inmbl 25577 iundisj2 25584 itg1addlem3 25733 fh1 31637 iundisj2f 32603 of0r 32688 iundisj2fi 32799 satffunlem1lem1 35407 satffunlem2lem1 35409 disjeccnvep 38285 disjecxrn 38390 br1cosscnvxrn 38475 |
| Copyright terms: Public domain | W3C validator |