Theorem ineq12 4165

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  ineq12i  4168  ineq12d  4171  ineqan12d  4172  fnun  6604  frrlem4  8229  undifixp  8870  endisj  8990  sbthlem8  9020  fiin  9323  pm54.43  9911  kmlem9  10067  indistopon  22943  epttop  22951  restbas  23100  ordtbas2  23133  txbas  23509  ptbasin  23519  trfbas2  23785  snfil  23806  fbasrn  23826  trfil2  23829  fmfnfmlem3  23898  ustuqtop2  24184  minveclem3b  25382  isperp  28733  brredunds  38822  diophin  42956  kelac2lem  43248  iscnrm3r  49135  incat  49788  setc1onsubc  49789