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 4181 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∩ cin 3932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 df-in 3940 |
This theorem is referenced by: funprg 6401 funtpg 6402 funcnvpr 6409 funcnvqp 6411 fvun1 6747 fndmin 6807 offval 7405 ofrfval 7406 offval3 7672 fpar 7800 offsplitfpar 7804 wfrlem4 7947 fisn 8879 ixxin 12743 vdwmc 16302 fvcosymgeq 18486 cssincl 20760 inmbl 24070 iundisj2 24077 itg1addlem3 24226 fh1 29322 iundisj2f 30268 iundisj2fi 30446 satffunlem1lem1 32546 satffunlem2lem1 32548 br1cosscnvxrn 35594 |
Copyright terms: Public domain | W3C validator |