Theorem ineq12d 4171

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3909

This theorem is referenced by:  csbin  4392  predeq123  6249  funcnvtp  6544  fnunres1  6593  ofrfvalg  7618  offval  7619  oev2  8438  isf32lem7  10250  ressval  17144  invffval  17665  invfval  17666  dfiso2  17679  isofn  17682  oppcinv  17687  zerooval  17902  cat1  18004  isps  18474  dmdprd  19913  dprddisj  19924  dprdf1o  19947  dmdprdsplit2lem  19960  dmdprdpr  19964  pgpfaclem1  19996  isunit  20292  dfrhm2  20393  isrhm  20397  rhmval  20416  2idlval  21189  pjfval  21644  aspval  21811  ressmplbas2  21963  isconn  23329  connsuba  23336  ptbasin  23493  ptclsg  23531  qtopval  23611  rnelfmlem  23868  trust  24145  isnmhm  24662  uniioombllem2a  25511  dyaddisjlem  25524  dyaddisj  25525  i1faddlem  25622  i1fmullem  25623  limcflf  25810  ewlksfval  29581  isewlk  29582  ewlkinedg  29584  ispth  29700  trlsegvdeg  30205  frcond3  30247  numclwwlk3lem2  30362  chocin  31473  cmbr3  31586  pjoml3  31590  fh1  31596  xppreima2  32631  cosnopne  32673  swrdrndisj  32936  hauseqcn  33909  prsssdm  33928  ordtrestNEW  33932  ordtrest2NEW  33934  cndprobval  34444  ballotlemfrc  34538  bnj1421  35052  satffunlem  35443  satffunlem1lem2  35445  satffunlem2lem1  35446  satffunlem2lem2  35448  msrval  35580  msrf  35584  ismfs  35591  clsun  36368  poimirlem8  37674  itg2addnclem2  37718  heiborlem4  37860  heiborlem6  37862  heiborlem10  37866  pmodl42N  39896  polfvalN  39949  poldmj1N  39973  pmapj2N  39974  pnonsingN  39978  psubclinN  39993  poml4N  39998  osumcllem9N  40009  trnfsetN  40200  diainN  41102  djaffvalN  41178  djafvalN  41179  djajN  41182  dihmeetcl  41390  dihmeet2  41391  dochnoncon  41436  djhffval  41441  djhfval  41442  djhlj  41446  dochdmm1  41455  lclkrlem2g  41558  lclkrlem2v  41573  lcfrlem21  41608  lcfrlem24  41611  mapdunirnN  41695  baerlem5amN  41761  baerlem5bmN  41762  baerlem5abmN  41763  mapdheq4lem  41776  mapdh6lem1N  41778  mapdh6lem2N  41779  hdmap1l6lem1  41852  hdmap1l6lem2  41853  aomclem8  43100  disjrnmpt2  45231  dvsinax  45957  dvcosax  45970  nnfoctbdjlem  46499  smfpimcc  46852  smfsuplem2  46856  upgrimpths  47946  iscnrm3l  48988  invfn  49068  invpropdlem  49076  infsubc2d  49100  zeroopropdlem  49280  zeroopropd  49283