Theorem ineq12d 4148

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895

This theorem is referenced by:  csbin  4374  predeq123  6207  funcnvtp  6504  ofrfvalg  7550  offval  7551  oev2  8362  isf32lem7  10124  ressval  16953  invffval  17479  invfval  17480  dfiso2  17493  isofn  17496  oppcinv  17501  zerooval  17719  cat1  17821  isps  18295  dmdprd  19610  dprddisj  19621  dprdf1o  19644  dmdprdsplit2lem  19657  dmdprdpr  19661  pgpfaclem1  19693  isunit  19908  dfrhm2  19970  isrhm  19974  2idlval  20513  pjfval  20922  aspval  21086  ressmplbas2  21237  isconn  22573  connsuba  22580  ptbasin  22737  ptclsg  22775  qtopval  22855  rnelfmlem  23112  trust  23390  isnmhm  23919  uniioombllem2a  24755  dyaddisjlem  24768  dyaddisj  24769  i1faddlem  24866  i1fmullem  24867  limcflf  25054  ewlksfval  27977  isewlk  27978  ewlkinedg  27980  ispth  28100  trlsegvdeg  28600  frcond3  28642  numclwwlk3lem2  28757  chocin  29866  cmbr3  29979  pjoml3  29983  fh1  29989  fnunres1  30954  xppreima2  30997  cosnopne  31036  swrdrndisj  31238  hauseqcn  31857  prsssdm  31876  ordtrestNEW  31880  ordtrest2NEW  31882  cndprobval  32409  ballotlemfrc  32502  bnj1421  33031  satffunlem  33372  satffunlem1lem2  33374  satffunlem2lem1  33375  satffunlem2lem2  33377  msrval  33509  msrf  33513  ismfs  33520  clsun  34526  poimirlem8  35794  itg2addnclem2  35838  heiborlem4  35981  heiborlem6  35983  heiborlem10  35987  pmodl42N  37872  polfvalN  37925  poldmj1N  37949  pmapj2N  37950  pnonsingN  37954  psubclinN  37969  poml4N  37974  osumcllem9N  37985  trnfsetN  38176  diainN  39078  djaffvalN  39154  djafvalN  39155  djajN  39158  dihmeetcl  39366  dihmeet2  39367  dochnoncon  39412  djhffval  39417  djhfval  39418  djhlj  39422  dochdmm1  39431  lclkrlem2g  39534  lclkrlem2v  39549  lcfrlem21  39584  lcfrlem24  39587  mapdunirnN  39671  baerlem5amN  39737  baerlem5bmN  39738  baerlem5abmN  39739  mapdheq4lem  39752  mapdh6lem1N  39754  mapdh6lem2N  39755  hdmap1l6lem1  39828  hdmap1l6lem2  39829  aomclem8  40893  disjrnmpt2  42733  dvsinax  43461  dvcosax  43474  nnfoctbdjlem  44000  smfpimcc  44352  smfsuplem2  44356  rhmval  45488  iscnrm3l  46256