Theorem ineq12 4156

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  ineq12i  4159  ineq12d  4162  ineqan12d  4163  fnun  6607  frrlem4  8233  undifixp  8876  endisj  8996  sbthlem8  9026  fiin  9329  pm54.43  9919  kmlem9  10075  indistopon  22979  epttop  22987  restbas  23136  ordtbas2  23169  txbas  23545  ptbasin  23555  trfbas2  23821  snfil  23842  fbasrn  23862  trfil2  23865  fmfnfmlem3  23934  ustuqtop2  24220  minveclem3b  25408  isperp  28797  brredunds  39048  eldisjim3  39153  diophin  43221  kelac2lem  43513  iscnrm3r  49438  incat  50091  setc1onsubc  50092