Theorem ineq12d 4175

Description: Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
ineq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
ineq12d	⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Proof of Theorem ineq12d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		ineq12 4169	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  csbin  4396  predeq123  6268  funcnvtp  6563  fnunres1  6612  ofrfvalg  7640  offval  7641  oev2  8460  isf32lem7  10281  ressval  17172  invffval  17694  invfval  17695  dfiso2  17708  isofn  17711  oppcinv  17716  zerooval  17931  cat1  18033  isps  18503  dmdprd  19941  dprddisj  19952  dprdf1o  19975  dmdprdsplit2lem  19988  dmdprdpr  19992  pgpfaclem1  20024  isunit  20321  dfrhm2  20422  isrhm  20426  rhmval  20445  2idlval  21218  pjfval  21673  aspval  21840  ressmplbas2  21994  isconn  23369  connsuba  23376  ptbasin  23533  ptclsg  23571  qtopval  23651  rnelfmlem  23908  trust  24185  isnmhm  24702  uniioombllem2a  25551  dyaddisjlem  25564  dyaddisj  25565  i1faddlem  25662  i1fmullem  25663  limcflf  25850  ewlksfval  29687  isewlk  29688  ewlkinedg  29690  ispth  29806  trlsegvdeg  30314  frcond3  30356  numclwwlk3lem2  30471  chocin  31582  cmbr3  31695  pjoml3  31699  fh1  31705  xppreima2  32740  cosnopne  32783  swrdrndisj  33049  hauseqcn  34075  prsssdm  34094  ordtrestNEW  34098  ordtrest2NEW  34100  cndprobval  34610  ballotlemfrc  34704  bnj1421  35217  satffunlem  35614  satffunlem1lem2  35616  satffunlem2lem1  35617  satffunlem2lem2  35619  msrval  35751  msrf  35755  ismfs  35762  clsun  36541  poimirlem8  37876  itg2addnclem2  37920  heiborlem4  38062  heiborlem6  38064  heiborlem10  38068  shiftstableeq2  38731  pmodl42N  40224  polfvalN  40277  poldmj1N  40301  pmapj2N  40302  pnonsingN  40306  psubclinN  40321  poml4N  40326  osumcllem9N  40337  trnfsetN  40528  diainN  41430  djaffvalN  41506  djafvalN  41507  djajN  41510  dihmeetcl  41718  dihmeet2  41719  dochnoncon  41764  djhffval  41769  djhfval  41770  djhlj  41774  dochdmm1  41783  lclkrlem2g  41886  lclkrlem2v  41901  lcfrlem21  41936  lcfrlem24  41939  mapdunirnN  42023  baerlem5amN  42089  baerlem5bmN  42090  baerlem5abmN  42091  mapdheq4lem  42104  mapdh6lem1N  42106  mapdh6lem2N  42107  hdmap1l6lem1  42180  hdmap1l6lem2  42181  aomclem8  43415  disjrnmpt2  45544  dvsinax  46268  dvcosax  46281  nnfoctbdjlem  46810  smfpimcc  47163  smfsuplem2  47167  upgrimpths  48266  iscnrm3l  49307  invfn  49386  invpropdlem  49394  infsubc2d  49418  zeroopropdlem  49598  zeroopropd  49601