Theorem ineq12 4161

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  ineq12i  4164  ineq12d  4167  ineqan12d  4168  vvin  4359  fnun  6653  frrlem4  8307  undifixp  8962  endisj  9083  sbthlem8  9113  fiin  9414  pm54.43  10082  kmlem9  10237  indistopon  23319  epttop  23327  restbas  23476  ordtbas2  23509  txbas  23886  ptbasin  23896  trfbas2  24162  snfil  24183  fbasrn  24203  trfil2  24206  fmfnfmlem3  24275  ustuqtop2  24561  minveclem3b  25749  isperp  29187  brprlng  29416  brredunds  39642  eldisjim3  39747  diophin  43782  kelac2lem  44065  iscnrm3r  50055  incat  50708  setc1onsubc  50709