Theorem ineq12 4208

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  ineq12i  4211  ineq12d  4214  ineqan12d  4215  fnun  6664  frrlem4  8274  undifixp  8928  endisj  9058  sbthlem8  9090  fiin  9417  pm54.43  9996  kmlem9  10153  indistopon  22504  epttop  22512  restbas  22662  ordtbas2  22695  txbas  23071  ptbasin  23081  trfbas2  23347  snfil  23368  fbasrn  23388  trfil2  23391  fmfnfmlem3  23460  ustuqtop2  23747  minveclem3b  24945  isperp  27963  brredunds  37496  diophin  41510  kelac2lem  41806  iscnrm3r  47581