Theorem ineq12d 4221

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  csbin  4442  predeq123  6322  funcnvtp  6629  fnunres1  6680  ofrfvalg  7705  offval  7706  oev2  8561  isf32lem7  10399  ressval  17277  invffval  17802  invfval  17803  dfiso2  17816  isofn  17819  oppcinv  17824  zerooval  18040  cat1  18142  isps  18613  dmdprd  20018  dprddisj  20029  dprdf1o  20052  dmdprdsplit2lem  20065  dmdprdpr  20069  pgpfaclem1  20101  isunit  20373  dfrhm2  20474  isrhm  20478  rhmval  20500  2idlval  21261  pjfval  21726  aspval  21893  ressmplbas2  22045  isconn  23421  connsuba  23428  ptbasin  23585  ptclsg  23623  qtopval  23703  rnelfmlem  23960  trust  24238  isnmhm  24767  uniioombllem2a  25617  dyaddisjlem  25630  dyaddisj  25631  i1faddlem  25728  i1fmullem  25729  limcflf  25916  ewlksfval  29619  isewlk  29620  ewlkinedg  29622  ispth  29741  trlsegvdeg  30246  frcond3  30288  numclwwlk3lem2  30403  chocin  31514  cmbr3  31627  pjoml3  31631  fh1  31637  xppreima2  32661  cosnopne  32703  swrdrndisj  32942  hauseqcn  33897  prsssdm  33916  ordtrestNEW  33920  ordtrest2NEW  33922  cndprobval  34435  ballotlemfrc  34529  bnj1421  35056  satffunlem  35406  satffunlem1lem2  35408  satffunlem2lem1  35409  satffunlem2lem2  35411  msrval  35543  msrf  35547  ismfs  35554  clsun  36329  poimirlem8  37635  itg2addnclem2  37679  heiborlem4  37821  heiborlem6  37823  heiborlem10  37827  pmodl42N  39853  polfvalN  39906  poldmj1N  39930  pmapj2N  39931  pnonsingN  39935  psubclinN  39950  poml4N  39955  osumcllem9N  39966  trnfsetN  40157  diainN  41059  djaffvalN  41135  djafvalN  41136  djajN  41139  dihmeetcl  41347  dihmeet2  41348  dochnoncon  41393  djhffval  41398  djhfval  41399  djhlj  41403  dochdmm1  41412  lclkrlem2g  41515  lclkrlem2v  41530  lcfrlem21  41565  lcfrlem24  41568  mapdunirnN  41652  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdheq4lem  41733  mapdh6lem1N  41735  mapdh6lem2N  41736  hdmap1l6lem1  41809  hdmap1l6lem2  41810  aomclem8  43073  disjrnmpt2  45193  dvsinax  45928  dvcosax  45941  nnfoctbdjlem  46470  smfpimcc  46823  smfsuplem2  46827  iscnrm3l  48848