Theorem ineq12 4166

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 4164	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		ineq2 4165	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷))
3	1, 2	sylan9eq 2784	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∩ cin 3902

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  ineq12i  4169  ineq12d  4172  ineqan12d  4173  fnun  6596  frrlem4  8222  undifixp  8861  endisj  8981  sbthlem8  9011  fiin  9312  pm54.43  9897  kmlem9  10053  indistopon  22886  epttop  22894  restbas  23043  ordtbas2  23076  txbas  23452  ptbasin  23462  trfbas2  23728  snfil  23749  fbasrn  23769  trfil2  23772  fmfnfmlem3  23841  ustuqtop2  24128  minveclem3b  25326  isperp  28657  brredunds  38607  diophin  42749  kelac2lem  43041  iscnrm3r  48936  incat  49590  setc1onsubc  49591