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 3809 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | syl2an 494 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∩ cin 3573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 |
This theorem is referenced by: funprg 5940 funtpg 5942 funcnvpr 5950 funcnvqp 5952 funcnvqpOLD 5953 fvun1 6269 fndmin 6324 offval 6904 ofrfval 6905 offval3 7162 fpar 7281 wfrlem4 7418 fisn 8333 ixxin 12192 vdwmc 15682 fvcosymgeq 17849 cssincl 20032 inmbl 23310 iundisj2 23317 itg1addlem3 23465 fh1 28477 iundisj2f 29403 iundisj2fi 29556 offval0 42299 |
Copyright terms: Public domain | W3C validator |