Theorem ineq12 4114

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-in 4093

This theorem is used by:  ineq12i  4117  ineq12d  4120  ineqan12d  4121  vvin  4361  fnun  6661  frrlem4  8318  undifixp  8973  endisj  9094  sbthlem8  9124  fiin  9424  pm54.43  10092  kmlem9  10247  indistopon  23331  epttop  23339  restbas  23488  ordtbas2  23521  txbas  23898  ptbasin  23908  trfbas2  24174  snfil  24195  fbasrn  24215  trfil2  24218  fmfnfmlem3  24287  ustuqtop2  24573  minveclem3b  25761  isperp  29199  brprlng  29428  brredunds  39782  eldisjim3  39887  diophin  43923  kelac2lem  44206  iscnrm3r  50201  incat  50878  setc1onsubc  50879