Theorem ineq12 4167

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  ineq12i  4170  ineq12d  4173  ineqan12d  4174  fnun  6606  frrlem4  8231  undifixp  8872  endisj  8992  sbthlem8  9022  fiin  9325  pm54.43  9913  kmlem9  10069  indistopon  22945  epttop  22953  restbas  23102  ordtbas2  23135  txbas  23511  ptbasin  23521  trfbas2  23787  snfil  23808  fbasrn  23828  trfil2  23831  fmfnfmlem3  23900  ustuqtop2  24186  minveclem3b  25384  isperp  28784  brredunds  38883  diophin  43014  kelac2lem  43306  iscnrm3r  49193  incat  49846  setc1onsubc  49847