Theorem ineq12d 4242

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

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  csbin  4465  predeq123  6333  funcnvtp  6641  fnunres1  6691  ofrfvalg  7722  offval  7723  oev2  8579  isf32lem7  10428  ressval  17290  invffval  17819  invfval  17820  dfiso2  17833  isofn  17836  oppcinv  17841  zerooval  18062  cat1  18164  isps  18638  dmdprd  20042  dprddisj  20053  dprdf1o  20076  dmdprdsplit2lem  20089  dmdprdpr  20093  pgpfaclem1  20125  isunit  20399  dfrhm2  20500  isrhm  20504  rhmval  20526  2idlval  21284  pjfval  21749  aspval  21916  ressmplbas2  22068  isconn  23442  connsuba  23449  ptbasin  23606  ptclsg  23644  qtopval  23724  rnelfmlem  23981  trust  24259  isnmhm  24788  uniioombllem2a  25636  dyaddisjlem  25649  dyaddisj  25650  i1faddlem  25747  i1fmullem  25748  limcflf  25936  ewlksfval  29637  isewlk  29638  ewlkinedg  29640  ispth  29759  trlsegvdeg  30259  frcond3  30301  numclwwlk3lem2  30416  chocin  31527  cmbr3  31640  pjoml3  31644  fh1  31650  xppreima2  32669  cosnopne  32706  swrdrndisj  32924  hauseqcn  33844  prsssdm  33863  ordtrestNEW  33867  ordtrest2NEW  33869  cndprobval  34398  ballotlemfrc  34491  bnj1421  35018  satffunlem  35369  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  msrval  35506  msrf  35510  ismfs  35517  clsun  36294  poimirlem8  37588  itg2addnclem2  37632  heiborlem4  37774  heiborlem6  37776  heiborlem10  37780  pmodl42N  39808  polfvalN  39861  poldmj1N  39885  pmapj2N  39886  pnonsingN  39890  psubclinN  39905  poml4N  39910  osumcllem9N  39921  trnfsetN  40112  diainN  41014  djaffvalN  41090  djafvalN  41091  djajN  41094  dihmeetcl  41302  dihmeet2  41303  dochnoncon  41348  djhffval  41353  djhfval  41354  djhlj  41358  dochdmm1  41367  lclkrlem2g  41470  lclkrlem2v  41485  lcfrlem21  41520  lcfrlem24  41523  mapdunirnN  41607  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdheq4lem  41688  mapdh6lem1N  41690  mapdh6lem2N  41691  hdmap1l6lem1  41764  hdmap1l6lem2  41765  aomclem8  43018  disjrnmpt2  45095  dvsinax  45834  dvcosax  45847  nnfoctbdjlem  46376  smfpimcc  46729  smfsuplem2  46733  iscnrm3l  48631