Theorem ineq12 4168

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  ineq12i  4171  ineq12d  4174  ineqan12d  4175  vvin  4366  fnun  6653  frrlem4  8292  undifixp  8938  endisj  9059  sbthlem8  9089  fiin  9389  pm54.43  10003  kmlem9  10158  indistopon  23210  epttop  23218  restbas  23367  ordtbas2  23400  txbas  23777  ptbasin  23787  trfbas2  24053  snfil  24074  fbasrn  24094  trfil2  24097  fmfnfmlem3  24166  ustuqtop2  24452  minveclem3b  25640  isperp  29045  brprlng  29245  brredunds  39419  eldisjim3  39524  diophin  43563  kelac2lem  43851  iscnrm3r  49785  incat  50438  setc1onsubc  50439