Theorem ineq12 4168

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  ineq12i  4171  ineq12d  4174  ineqan12d  4175  vvin  4366  fnun  6649  frrlem4  8282  undifixp  8928  endisj  9048  sbthlem8  9078  fiin  9378  pm54.43  9983  kmlem9  10138  indistopon  23158  epttop  23166  restbas  23315  ordtbas2  23348  txbas  23724  ptbasin  23734  trfbas2  24000  snfil  24021  fbasrn  24041  trfil2  24044  fmfnfmlem3  24113  ustuqtop2  24399  minveclem3b  25587  isperp  28992  brprlng  29188  brredunds  39379  eldisjim3  39484  diophin  43523  kelac2lem  43811  iscnrm3r  49746  incat  50399  setc1onsubc  50400