Theorem ineq12 4115

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  ineq12i  4118  ineq12d  4121  ineqan12d  4122  vvin  4362  fnun  6683  frrlem4  8345  undifixp  9000  endisj  9121  sbthlem8  9151  fiin  9451  pm54.43  10121  kmlem9  10276  indistopon  23374  epttop  23382  restbas  23531  ordtbas2  23564  txbas  23941  ptbasin  23951  trfbas2  24217  snfil  24238  fbasrn  24258  trfil2  24261  fmfnfmlem3  24330  ustuqtop2  24616  minveclem3b  25804  isperp  29244  brprlng  29473  brredunds  39908  eldisjim3  40013  diophin  44049  kelac2lem  44332  iscnrm3r  50393  incat  51070  setc1onsubc  51071