Theorem ineq12 4176

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  ineq12i  4179  ineq12d  4182  ineqan12d  4183  vvin  4372  fnun  6650  frrlem4  8286  undifixp  8932  endisj  9052  sbthlem8  9082  fiin  9382  pm54.43  9987  kmlem9  10142  indistopon  23127  epttop  23135  restbas  23284  ordtbas2  23317  txbas  23693  ptbasin  23703  trfbas2  23969  snfil  23990  fbasrn  24010  trfil2  24013  fmfnfmlem3  24082  ustuqtop2  24368  minveclem3b  25556  isperp  28951  brprlng  29143  brredunds  39249  eldisjim3  39354  diophin  43395  kelac2lem  43683  iscnrm3r  49611  incat  50264  setc1onsubc  50265