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

Theorem ineq12 4215
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 4213 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 4214 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2797 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958
This theorem is referenced by:  ineq12i  4218  ineq12d  4221  ineqan12d  4222  fnun  6682  frrlem4  8314  undifixp  8974  endisj  9098  sbthlem8  9130  fiin  9462  pm54.43  10041  kmlem9  10199  indistopon  23008  epttop  23016  restbas  23166  ordtbas2  23199  txbas  23575  ptbasin  23585  trfbas2  23851  snfil  23872  fbasrn  23892  trfil2  23895  fmfnfmlem3  23964  ustuqtop2  24251  minveclem3b  25462  isperp  28720  brredunds  38627  diophin  42783  kelac2lem  43076  iscnrm3r  48845
  Copyright terms: Public domain W3C validator