Theorem ineq12d 4150

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

Syntax hints:   → wi 4   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  csbin  4370  predeq123  6253  funcnvtp  6548  fnunres1  6597  ofrfvalg  7628  offval  7629  oev2  8448  isf32lem7  10272  ressval  17194  invffval  17716  invfval  17717  dfiso2  17730  isofn  17733  oppcinv  17738  zerooval  17953  cat1  18055  isps  18525  dmdprd  19966  dprddisj  19977  dprdf1o  20000  dmdprdsplit2lem  20013  dmdprdpr  20017  pgpfaclem1  20049  isunit  20344  dfrhm2  20445  isrhm  20449  rhmval  20471  2idlval  21244  pjfval  21681  aspval  21847  ressmplbas2  22002  isconn  23396  connsuba  23403  ptbasin  23560  ptclsg  23598  qtopval  23678  rnelfmlem  23935  trust  24212  isnmhm  24729  uniioombllem2a  25567  dyaddisjlem  25580  dyaddisj  25581  i1faddlem  25678  i1fmullem  25679  limcflf  25866  ewlksfval  29688  isewlk  29689  ewlkinedg  29691  ispth  29807  trlsegvdeg  30315  frcond3  30357  numclwwlk3lem2  30472  chocin  31584  cmbr3  31697  pjoml3  31701  fh1  31707  xppreima2  32743  cosnopne  32786  swrdrndisj  33036  hauseqcn  34082  prsssdm  34101  ordtrestNEW  34105  ordtrest2NEW  34107  cndprobval  34617  ballotlemfrc  34711  bnj1421  35224  satffunlem  35629  satffunlem1lem2  35631  satffunlem2lem1  35632  satffunlem2lem2  35634  msrval  35766  msrf  35770  ismfs  35777  clsun  36556  poimirlem8  37995  itg2addnclem2  38039  heiborlem4  38181  heiborlem6  38183  heiborlem10  38187  shiftstableeq2  38850  pmodl42N  40343  polfvalN  40396  poldmj1N  40420  pmapj2N  40421  pnonsingN  40425  psubclinN  40440  poml4N  40445  osumcllem9N  40456  trnfsetN  40647  diainN  41549  djaffvalN  41625  djafvalN  41626  djajN  41629  dihmeetcl  41837  dihmeet2  41838  dochnoncon  41883  djhffval  41888  djhfval  41889  djhlj  41893  dochdmm1  41902  lclkrlem2g  42005  lclkrlem2v  42020  lcfrlem21  42055  lcfrlem24  42058  mapdunirnN  42142  baerlem5amN  42208  baerlem5bmN  42209  baerlem5abmN  42210  mapdheq4lem  42223  mapdh6lem1N  42225  mapdh6lem2N  42226  hdmap1l6lem1  42299  hdmap1l6lem2  42300  aomclem8  43506  disjrnmpt2  45635  dvsinax  46356  dvcosax  46369  nnfoctbdjlem  46898  smfpimcc  47251  smfsuplem2  47255  upgrimpths  48400  iscnrm3l  49441  invfn  49520  invpropdlem  49528  infsubc2d  49552  zeroopropdlem  49732  zeroopropd  49735