Theorem ineq12 4195

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  ineq12i  4198  ineq12d  4201  ineqan12d  4202  fnun  6657  frrlem4  8293  undifixp  8953  endisj  9077  sbthlem8  9109  fiin  9439  pm54.43  10020  kmlem9  10178  indistopon  22944  epttop  22952  restbas  23101  ordtbas2  23134  txbas  23510  ptbasin  23520  trfbas2  23786  snfil  23807  fbasrn  23827  trfil2  23830  fmfnfmlem3  23899  ustuqtop2  24186  minveclem3b  25385  isperp  28696  brredunds  38649  diophin  42762  kelac2lem  43055  iscnrm3r  48889  incat  49445  setc1onsubc  49446