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

Theorem ineq12 4032
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 4030 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 4031 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2834 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  cin 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799
This theorem is referenced by:  ineq12i  4035  ineq12d  4038  ineqan12d  4039  fnun  6243  undifixp  8230  endisj  8335  sbthlem8  8365  fiin  8616  pm54.43  9159  kmlem9  9315  indistopon  21213  epttop  21221  restbas  21370  ordtbas2  21403  txbas  21779  ptbasin  21789  trfbas2  22055  snfil  22076  fbasrn  22096  trfil2  22099  fmfnfmlem3  22168  ustuqtop2  22454  minveclem3b  23634  isperp  26063  frrlem4  32372  brreds  34997  diophin  38300  kelac2lem  38597
  Copyright terms: Public domain W3C validator