Theorem ineq12d 4180

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  csbin  4401  predeq123  6263  funcnvtp  6563  fnunres1  6612  ofrfvalg  7641  offval  7642  oev2  8464  isf32lem7  10288  ressval  17179  invffval  17696  invfval  17697  dfiso2  17710  isofn  17713  oppcinv  17718  zerooval  17933  cat1  18035  isps  18503  dmdprd  19906  dprddisj  19917  dprdf1o  19940  dmdprdsplit2lem  19953  dmdprdpr  19957  pgpfaclem1  19989  isunit  20258  dfrhm2  20359  isrhm  20363  rhmval  20385  2idlval  21137  pjfval  21591  aspval  21758  ressmplbas2  21910  isconn  23276  connsuba  23283  ptbasin  23440  ptclsg  23478  qtopval  23558  rnelfmlem  23815  trust  24093  isnmhm  24610  uniioombllem2a  25459  dyaddisjlem  25472  dyaddisj  25473  i1faddlem  25570  i1fmullem  25571  limcflf  25758  ewlksfval  29505  isewlk  29506  ewlkinedg  29508  ispth  29624  trlsegvdeg  30129  frcond3  30171  numclwwlk3lem2  30286  chocin  31397  cmbr3  31510  pjoml3  31514  fh1  31520  xppreima2  32548  cosnopne  32590  swrdrndisj  32852  hauseqcn  33861  prsssdm  33880  ordtrestNEW  33884  ordtrest2NEW  33886  cndprobval  34397  ballotlemfrc  34491  bnj1421  35005  satffunlem  35361  satffunlem1lem2  35363  satffunlem2lem1  35364  satffunlem2lem2  35366  msrval  35498  msrf  35502  ismfs  35509  clsun  36289  poimirlem8  37595  itg2addnclem2  37639  heiborlem4  37781  heiborlem6  37783  heiborlem10  37787  pmodl42N  39818  polfvalN  39871  poldmj1N  39895  pmapj2N  39896  pnonsingN  39900  psubclinN  39915  poml4N  39920  osumcllem9N  39931  trnfsetN  40122  diainN  41024  djaffvalN  41100  djafvalN  41101  djajN  41104  dihmeetcl  41312  dihmeet2  41313  dochnoncon  41358  djhffval  41363  djhfval  41364  djhlj  41368  dochdmm1  41377  lclkrlem2g  41480  lclkrlem2v  41495  lcfrlem21  41530  lcfrlem24  41533  mapdunirnN  41617  baerlem5amN  41683  baerlem5bmN  41684  baerlem5abmN  41685  mapdheq4lem  41698  mapdh6lem1N  41700  mapdh6lem2N  41701  hdmap1l6lem1  41774  hdmap1l6lem2  41775  aomclem8  43023  disjrnmpt2  45155  dvsinax  45884  dvcosax  45897  nnfoctbdjlem  46426  smfpimcc  46779  smfsuplem2  46783  upgrimpths  47882  iscnrm3l  48912  invfn  48992  invpropdlem  49000  infsubc2d  49024  zeroopropdlem  49204  zeroopropd  49207