Theorem ineq12d 4162

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  csbin  4383  predeq123  6260  funcnvtp  6555  fnunres1  6604  ofrfvalg  7632  offval  7633  oev2  8451  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  20468  2idlval  21241  pjfval  21696  aspval  21862  ressmplbas2  22015  isconn  23388  connsuba  23395  ptbasin  23552  ptclsg  23590  qtopval  23670  rnelfmlem  23927  trust  24204  isnmhm  24721  uniioombllem2a  25559  dyaddisjlem  25572  dyaddisj  25573  i1faddlem  25670  i1fmullem  25671  limcflf  25858  ewlksfval  29685  isewlk  29686  ewlkinedg  29688  ispth  29804  trlsegvdeg  30312  frcond3  30354  numclwwlk3lem2  30469  chocin  31581  cmbr3  31694  pjoml3  31698  fh1  31704  xppreima2  32739  cosnopne  32782  swrdrndisj  33032  hauseqcn  34058  prsssdm  34077  ordtrestNEW  34081  ordtrest2NEW  34083  cndprobval  34593  ballotlemfrc  34687  bnj1421  35200  satffunlem  35599  satffunlem1lem2  35601  satffunlem2lem1  35602  satffunlem2lem2  35604  msrval  35736  msrf  35740  ismfs  35747  clsun  36526  poimirlem8  37963  itg2addnclem2  38007  heiborlem4  38149  heiborlem6  38151  heiborlem10  38155  shiftstableeq2  38818  pmodl42N  40311  polfvalN  40364  poldmj1N  40388  pmapj2N  40389  pnonsingN  40393  psubclinN  40408  poml4N  40413  osumcllem9N  40424  trnfsetN  40615  diainN  41517  djaffvalN  41593  djafvalN  41594  djajN  41597  dihmeetcl  41805  dihmeet2  41806  dochnoncon  41851  djhffval  41856  djhfval  41857  djhlj  41861  dochdmm1  41870  lclkrlem2g  41973  lclkrlem2v  41988  lcfrlem21  42023  lcfrlem24  42026  mapdunirnN  42110  baerlem5amN  42176  baerlem5bmN  42177  baerlem5abmN  42178  mapdheq4lem  42191  mapdh6lem1N  42193  mapdh6lem2N  42194  hdmap1l6lem1  42267  hdmap1l6lem2  42268  aomclem8  43507  disjrnmpt2  45636  dvsinax  46359  dvcosax  46372  nnfoctbdjlem  46901  smfpimcc  47254  smfsuplem2  47258  upgrimpths  48397  iscnrm3l  49438  invfn  49517  invpropdlem  49525  infsubc2d  49549  zeroopropdlem  49729  zeroopropd  49732