Theorem ineq12 4183

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942

This theorem is referenced by:  ineq12i  4186  ineq12d  4189  ineqan12d  4190  fnun  6457  undifixp  8492  endisj  8598  sbthlem8  8628  fiin  8880  pm54.43  9423  kmlem9  9578  indistopon  21603  epttop  21611  restbas  21760  ordtbas2  21793  txbas  22169  ptbasin  22179  trfbas2  22445  snfil  22466  fbasrn  22486  trfil2  22489  fmfnfmlem3  22558  ustuqtop2  22845  minveclem3b  24025  isperp  26492  frrlem4  33121  brredunds  35855  diophin  39362  kelac2lem  39657