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 2815	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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  ineq12i  4164  ineq12d  4167  ineqan12d  4168  vvin  4359  fnun  6647  frrlem4  8289  undifixp  8942  endisj  9063  sbthlem8  9093  fiin  9393  pm54.43  10007  kmlem9  10162  indistopon  23227  epttop  23235  restbas  23384  ordtbas2  23417  txbas  23794  ptbasin  23804  trfbas2  24070  snfil  24091  fbasrn  24111  trfil2  24114  fmfnfmlem3  24183  ustuqtop2  24469  minveclem3b  25657  isperp  29067  brprlng  29296  brredunds  39459  eldisjim3  39564  diophin  43618  kelac2lem  43906  iscnrm3r  49875  incat  50528  setc1onsubc  50529