Theorem ineq12d 4170

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905

This theorem is referenced by:  csbin  4391  predeq123  6257  funcnvtp  6552  fnunres1  6601  ofrfvalg  7627  offval  7628  oev2  8447  isf32lem7  10261  ressval  17151  invffval  17673  invfval  17674  dfiso2  17687  isofn  17690  oppcinv  17695  zerooval  17910  cat1  18012  isps  18482  dmdprd  19920  dprddisj  19931  dprdf1o  19954  dmdprdsplit2lem  19967  dmdprdpr  19971  pgpfaclem1  20003  isunit  20300  dfrhm2  20401  isrhm  20405  rhmval  20424  2idlval  21197  pjfval  21652  aspval  21819  ressmplbas2  21973  isconn  23348  connsuba  23355  ptbasin  23512  ptclsg  23550  qtopval  23630  rnelfmlem  23887  trust  24164  isnmhm  24681  uniioombllem2a  25530  dyaddisjlem  25543  dyaddisj  25544  i1faddlem  25641  i1fmullem  25642  limcflf  25829  ewlksfval  29601  isewlk  29602  ewlkinedg  29604  ispth  29720  trlsegvdeg  30228  frcond3  30270  numclwwlk3lem2  30385  chocin  31496  cmbr3  31609  pjoml3  31613  fh1  31619  xppreima2  32655  cosnopne  32699  swrdrndisj  32967  hauseqcn  33983  prsssdm  34002  ordtrestNEW  34006  ordtrest2NEW  34008  cndprobval  34518  ballotlemfrc  34612  bnj1421  35126  satffunlem  35517  satffunlem1lem2  35519  satffunlem2lem1  35520  satffunlem2lem2  35522  msrval  35654  msrf  35658  ismfs  35665  clsun  36444  poimirlem8  37741  itg2addnclem2  37785  heiborlem4  37927  heiborlem6  37929  heiborlem10  37933  pmodl42N  40023  polfvalN  40076  poldmj1N  40100  pmapj2N  40101  pnonsingN  40105  psubclinN  40120  poml4N  40125  osumcllem9N  40136  trnfsetN  40327  diainN  41229  djaffvalN  41305  djafvalN  41306  djajN  41309  dihmeetcl  41517  dihmeet2  41518  dochnoncon  41563  djhffval  41568  djhfval  41569  djhlj  41573  dochdmm1  41582  lclkrlem2g  41685  lclkrlem2v  41700  lcfrlem21  41735  lcfrlem24  41738  mapdunirnN  41822  baerlem5amN  41888  baerlem5bmN  41889  baerlem5abmN  41890  mapdheq4lem  41903  mapdh6lem1N  41905  mapdh6lem2N  41906  hdmap1l6lem1  41979  hdmap1l6lem2  41980  aomclem8  43218  disjrnmpt2  45348  dvsinax  46073  dvcosax  46086  nnfoctbdjlem  46615  smfpimcc  46968  smfsuplem2  46972  upgrimpths  48071  iscnrm3l  49112  invfn  49191  invpropdlem  49199  infsubc2d  49223  zeroopropdlem  49403  zeroopropd  49406