Theorem ineq12 4215

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  ineq12i  4218  ineq12d  4221  ineqan12d  4222  fnun  6682  frrlem4  8314  undifixp  8974  endisj  9098  sbthlem8  9130  fiin  9462  pm54.43  10041  kmlem9  10199  indistopon  23008  epttop  23016  restbas  23166  ordtbas2  23199  txbas  23575  ptbasin  23585  trfbas2  23851  snfil  23872  fbasrn  23892  trfil2  23895  fmfnfmlem3  23964  ustuqtop2  24251  minveclem3b  25462  isperp  28720  brredunds  38627  diophin  42783  kelac2lem  43076  iscnrm3r  48845