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

Theorem ineq12 4158
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 4155 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 4157 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2877 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  cin 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-rab 3139  df-in 3915
This theorem is referenced by:  ineq12i  4161  ineq12d  4164  ineqan12d  4165  fnun  6443  undifixp  8485  endisj  8591  sbthlem8  8622  fiin  8874  pm54.43  9418  kmlem9  9573  indistopon  21604  epttop  21612  restbas  21761  ordtbas2  21794  txbas  22170  ptbasin  22180  trfbas2  22446  snfil  22467  fbasrn  22487  trfil2  22490  fmfnfmlem3  22559  ustuqtop2  22846  minveclem3b  24030  isperp  26504  frrlem4  33200  brredunds  35979  diophin  39643  kelac2lem  39938
  Copyright terms: Public domain W3C validator