Theorem ineq12d 4161

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  csbin  4382  predeq123  6266  funcnvtp  6561  fnunres1  6610  ofrfvalg  7639  offval  7640  oev2  8458  isf32lem7  10281  ressval  17203  invffval  17725  invfval  17726  dfiso2  17739  isofn  17742  oppcinv  17747  zerooval  17962  cat1  18064  isps  18534  dmdprd  19975  dprddisj  19986  dprdf1o  20009  dmdprdsplit2lem  20022  dmdprdpr  20026  pgpfaclem1  20058  isunit  20353  dfrhm2  20454  isrhm  20458  rhmval  20477  2idlval  21249  pjfval  21686  aspval  21852  ressmplbas2  22005  isconn  23378  connsuba  23385  ptbasin  23542  ptclsg  23580  qtopval  23660  rnelfmlem  23917  trust  24194  isnmhm  24711  uniioombllem2a  25549  dyaddisjlem  25562  dyaddisj  25563  i1faddlem  25660  i1fmullem  25661  limcflf  25848  ewlksfval  29670  isewlk  29671  ewlkinedg  29673  ispth  29789  trlsegvdeg  30297  frcond3  30339  numclwwlk3lem2  30454  chocin  31566  cmbr3  31679  pjoml3  31683  fh1  31689  xppreima2  32724  cosnopne  32767  swrdrndisj  33017  hauseqcn  34042  prsssdm  34061  ordtrestNEW  34065  ordtrest2NEW  34067  cndprobval  34577  ballotlemfrc  34671  bnj1421  35184  satffunlem  35583  satffunlem1lem2  35585  satffunlem2lem1  35586  satffunlem2lem2  35588  msrval  35720  msrf  35724  ismfs  35731  clsun  36510  poimirlem8  37949  itg2addnclem2  37993  heiborlem4  38135  heiborlem6  38137  heiborlem10  38141  shiftstableeq2  38804  pmodl42N  40297  polfvalN  40350  poldmj1N  40374  pmapj2N  40375  pnonsingN  40379  psubclinN  40394  poml4N  40399  osumcllem9N  40410  trnfsetN  40601  diainN  41503  djaffvalN  41579  djafvalN  41580  djajN  41583  dihmeetcl  41791  dihmeet2  41792  dochnoncon  41837  djhffval  41842  djhfval  41843  djhlj  41847  dochdmm1  41856  lclkrlem2g  41959  lclkrlem2v  41974  lcfrlem21  42009  lcfrlem24  42012  mapdunirnN  42096  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdheq4lem  42177  mapdh6lem1N  42179  mapdh6lem2N  42180  hdmap1l6lem1  42253  hdmap1l6lem2  42254  aomclem8  43489  disjrnmpt2  45618  dvsinax  46341  dvcosax  46354  nnfoctbdjlem  46883  smfpimcc  47236  smfsuplem2  47240  upgrimpths  48385  iscnrm3l  49426  invfn  49505  invpropdlem  49513  infsubc2d  49537  zeroopropdlem  49717  zeroopropd  49720