Theorem ineq12 4155

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  ineq12i  4158  ineq12d  4161  ineqan12d  4162  fnun  6612  frrlem4  8239  undifixp  8882  endisj  9002  sbthlem8  9032  fiin  9335  pm54.43  9925  kmlem9  10081  indistopon  22966  epttop  22974  restbas  23123  ordtbas2  23156  txbas  23532  ptbasin  23542  trfbas2  23808  snfil  23829  fbasrn  23849  trfil2  23852  fmfnfmlem3  23921  ustuqtop2  24207  minveclem3b  25395  isperp  28780  brredunds  39031  eldisjim3  39136  diophin  43204  kelac2lem  43492  iscnrm3r  49423  incat  50076  setc1onsubc  50077