Theorem ineq12 4138

Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)

Assertion

Ref	Expression
ineq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 4136	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		ineq2 4137	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷))
3	1, 2	sylan9eq 2799	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  ineq12i  4141  ineq12d  4144  ineqan12d  4145  fnun  6529  frrlem4  8076  undifixp  8680  endisj  8799  sbthlem8  8830  fiin  9111  pm54.43  9690  kmlem9  9845  indistopon  22059  epttop  22067  restbas  22217  ordtbas2  22250  txbas  22626  ptbasin  22636  trfbas2  22902  snfil  22923  fbasrn  22943  trfil2  22946  fmfnfmlem3  23015  ustuqtop2  23302  minveclem3b  24497  isperp  26977  brredunds  36666  diophin  40510  kelac2lem  40805  iscnrm3r  46130