Theorem ineq12 4223

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∩ cin 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970

This theorem is referenced by:  ineq12i  4226  ineq12d  4229  ineqan12d  4230  fnun  6683  frrlem4  8313  undifixp  8973  endisj  9097  sbthlem8  9129  fiin  9460  pm54.43  10039  kmlem9  10197  indistopon  23024  epttop  23032  restbas  23182  ordtbas2  23215  txbas  23591  ptbasin  23601  trfbas2  23867  snfil  23888  fbasrn  23908  trfil2  23911  fmfnfmlem3  23980  ustuqtop2  24267  minveclem3b  25476  isperp  28735  brredunds  38608  diophin  42760  kelac2lem  43053  iscnrm3r  48745