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

Theorem ineq12 3801
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 3799 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 ineq2 3800 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2674 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  cin 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574
This theorem is referenced by:  ineq12i  3804  ineq12d  3807  ineqan12d  3808  fnun  5985  undifixp  7929  endisj  8032  sbthlem8  8062  fiin  8313  pm54.43  8811  kmlem9  8965  indistopon  20786  epttop  20794  restbas  20943  ordtbas2  20976  txbas  21351  ptbasin  21361  trfbas2  21628  snfil  21649  fbasrn  21669  trfil2  21672  fmfnfmlem3  21741  ustuqtop2  22027  minveclem3b  23180  isperp  25588  frrlem4  31757  diophin  37155  kelac2lem  37453
  Copyright terms: Public domain W3C validator