Theorem ineq12d 4173

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 4167	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3900

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  csbin  4394  predeq123  6260  funcnvtp  6555  fnunres1  6604  ofrfvalg  7630  offval  7631  oev2  8450  isf32lem7  10269  ressval  17160  invffval  17682  invfval  17683  dfiso2  17696  isofn  17699  oppcinv  17704  zerooval  17919  cat1  18021  isps  18491  dmdprd  19929  dprddisj  19940  dprdf1o  19963  dmdprdsplit2lem  19976  dmdprdpr  19980  pgpfaclem1  20012  isunit  20309  dfrhm2  20410  isrhm  20414  rhmval  20433  2idlval  21206  pjfval  21661  aspval  21828  ressmplbas2  21982  isconn  23357  connsuba  23364  ptbasin  23521  ptclsg  23559  qtopval  23639  rnelfmlem  23896  trust  24173  isnmhm  24690  uniioombllem2a  25539  dyaddisjlem  25552  dyaddisj  25553  i1faddlem  25650  i1fmullem  25651  limcflf  25838  ewlksfval  29675  isewlk  29676  ewlkinedg  29678  ispth  29794  trlsegvdeg  30302  frcond3  30344  numclwwlk3lem2  30459  chocin  31570  cmbr3  31683  pjoml3  31687  fh1  31693  xppreima2  32729  cosnopne  32773  swrdrndisj  33039  hauseqcn  34055  prsssdm  34074  ordtrestNEW  34078  ordtrest2NEW  34080  cndprobval  34590  ballotlemfrc  34684  bnj1421  35198  satffunlem  35595  satffunlem1lem2  35597  satffunlem2lem1  35598  satffunlem2lem2  35600  msrval  35732  msrf  35736  ismfs  35743  clsun  36522  poimirlem8  37829  itg2addnclem2  37873  heiborlem4  38015  heiborlem6  38017  heiborlem10  38021  pmodl42N  40111  polfvalN  40164  poldmj1N  40188  pmapj2N  40189  pnonsingN  40193  psubclinN  40208  poml4N  40213  osumcllem9N  40224  trnfsetN  40415  diainN  41317  djaffvalN  41393  djafvalN  41394  djajN  41397  dihmeetcl  41605  dihmeet2  41606  dochnoncon  41651  djhffval  41656  djhfval  41657  djhlj  41661  dochdmm1  41670  lclkrlem2g  41773  lclkrlem2v  41788  lcfrlem21  41823  lcfrlem24  41826  mapdunirnN  41910  baerlem5amN  41976  baerlem5bmN  41977  baerlem5abmN  41978  mapdheq4lem  41991  mapdh6lem1N  41993  mapdh6lem2N  41994  hdmap1l6lem1  42067  hdmap1l6lem2  42068  aomclem8  43303  disjrnmpt2  45432  dvsinax  46157  dvcosax  46170  nnfoctbdjlem  46699  smfpimcc  47052  smfsuplem2  47056  upgrimpths  48155  iscnrm3l  49196  invfn  49275  invpropdlem  49283  infsubc2d  49307  zeroopropdlem  49487  zeroopropd  49490