Theorem ineq12 4205

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∩ cin 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-in 3951

This theorem is referenced by:  ineq12i  4208  ineq12d  4211  ineqan12d  4212  fnun  6669  frrlem4  8295  undifixp  8953  endisj  9083  sbthlem8  9115  fiin  9447  pm54.43  10026  kmlem9  10183  indistopon  22948  epttop  22956  restbas  23106  ordtbas2  23139  txbas  23515  ptbasin  23525  trfbas2  23791  snfil  23812  fbasrn  23832  trfil2  23835  fmfnfmlem3  23904  ustuqtop2  24191  minveclem3b  25400  isperp  28588  brredunds  38228  diophin  42334  kelac2lem  42630  iscnrm3r  48153