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  22921  epttop  22929  restbas  23078  ordtbas2  23111  txbas  23487  ptbasin  23497  trfbas2  23763  snfil  23784  fbasrn  23804  trfil2  23807  fmfnfmlem3  23876  ustuqtop2  24163  minveclem3b  25361  isperp  28692  brredunds  38610  diophin  42753  kelac2lem  43046  iscnrm3r  48929  incat  49583  setc1onsubc  49584