Theorem ineq12 4147

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-in 3892

This theorem is referenced by:  ineq12i  4150  ineq12d  4153  ineqan12d  4154  fnun  6603  frrlem4  8233  undifixp  8876  endisj  8996  sbthlem8  9026  fiin  9329  pm54.43  9920  kmlem9  10076  indistopon  22988  epttop  22996  restbas  23145  ordtbas2  23178  txbas  23554  ptbasin  23564  trfbas2  23830  snfil  23851  fbasrn  23871  trfil2  23874  fmfnfmlem3  23943  ustuqtop2  24229  minveclem3b  25417  isperp  28802  brredunds  39092  eldisjim3  39197  diophin  43236  kelac2lem  43524  iscnrm3r  49452  incat  50105  setc1onsubc  50106