Theorem ineq12 4174

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

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

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 3403  df-in 3918

This theorem is referenced by:  ineq12i  4177  ineq12d  4180  ineqan12d  4181  fnun  6614  frrlem4  8245  undifixp  8884  endisj  9005  sbthlem8  9035  fiin  9349  pm54.43  9930  kmlem9  10088  indistopon  22864  epttop  22872  restbas  23021  ordtbas2  23054  txbas  23430  ptbasin  23440  trfbas2  23706  snfil  23727  fbasrn  23747  trfil2  23750  fmfnfmlem3  23819  ustuqtop2  24106  minveclem3b  25304  isperp  28615  brredunds  38590  diophin  42733  kelac2lem  43026  iscnrm3r  48909  incat  49563  setc1onsubc  49564