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

Theorem ineq12 4172
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 4170 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 4171 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2797 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  cin 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-in 3922
This theorem is referenced by:  ineq12i  4175  ineq12d  4178  ineqan12d  4179  fnun  6619  frrlem4  8225  undifixp  8879  endisj  9009  sbthlem8  9041  fiin  9365  pm54.43  9944  kmlem9  10101  indistopon  22367  epttop  22375  restbas  22525  ordtbas2  22558  txbas  22934  ptbasin  22944  trfbas2  23210  snfil  23231  fbasrn  23251  trfil2  23254  fmfnfmlem3  23323  ustuqtop2  23610  minveclem3b  24808  isperp  27696  brredunds  37117  diophin  41124  kelac2lem  41420  iscnrm3r  47055
  Copyright terms: Public domain W3C validator