Theorem ineq12 4167

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  ineq12i  4170  ineq12d  4173  ineqan12d  4174  fnun  6635  frrlem4  8270  undifixp  8916  endisj  9036  sbthlem8  9066  fiin  9368  pm54.43  9959  kmlem9  10115  indistopon  23061  epttop  23069  restbas  23218  ordtbas2  23251  txbas  23627  ptbasin  23637  trfbas2  23903  snfil  23924  fbasrn  23944  trfil2  23947  fmfnfmlem3  24016  ustuqtop2  24302  minveclem3b  25490  isperp  28885  brprlng  29065  brredunds  39209  eldisjim3  39314  diophin  43353  kelac2lem  43641  iscnrm3r  49569  incat  50222  setc1onsubc  50223