MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq12 Structured version   Visualization version   GIF version

Theorem ineq12 4205
Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
Assertion
Ref Expression
ineq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem ineq12
StepHypRef Expression
1 ineq1 4203 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 4204 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2785 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = 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-in 3951
This theorem is referenced by:  ineq12i  4208  ineq12d  4211  ineqan12d  4212  fnun  6669  frrlem4  8295  undifixp  8953  endisj  9083  sbthlem8  9115  fiin  9447  pm54.43  10026  kmlem9  10183  indistopon  22948  epttop  22956  restbas  23106  ordtbas2  23139  txbas  23515  ptbasin  23525  trfbas2  23791  snfil  23812  fbasrn  23832  trfil2  23835  fmfnfmlem3  23904  ustuqtop2  24191  minveclem3b  25400  isperp  28588  brredunds  38228  diophin  42334  kelac2lem  42630  iscnrm3r  48153
  Copyright terms: Public domain W3C validator