Theorem ineq12d 4213

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955

This theorem is referenced by:  csbin  4439  predeq123  6301  funcnvtp  6611  fnunres1  6661  ofrfvalg  7677  offval  7678  oev2  8522  isf32lem7  10353  ressval  17175  invffval  17704  invfval  17705  dfiso2  17718  isofn  17721  oppcinv  17726  zerooval  17944  cat1  18046  isps  18520  dmdprd  19867  dprddisj  19878  dprdf1o  19901  dmdprdsplit2lem  19914  dmdprdpr  19918  pgpfaclem1  19950  isunit  20186  dfrhm2  20252  isrhm  20256  2idlval  20857  pjfval  21260  aspval  21426  ressmplbas2  21581  isconn  22916  connsuba  22923  ptbasin  23080  ptclsg  23118  qtopval  23198  rnelfmlem  23455  trust  23733  isnmhm  24262  uniioombllem2a  25098  dyaddisjlem  25111  dyaddisj  25112  i1faddlem  25209  i1fmullem  25210  limcflf  25397  ewlksfval  28855  isewlk  28856  ewlkinedg  28858  ispth  28977  trlsegvdeg  29477  frcond3  29519  numclwwlk3lem2  29634  chocin  30743  cmbr3  30856  pjoml3  30860  fh1  30866  xppreima2  31871  cosnopne  31911  swrdrndisj  32116  hauseqcn  32873  prsssdm  32892  ordtrestNEW  32896  ordtrest2NEW  32898  cndprobval  33427  ballotlemfrc  33520  bnj1421  34048  satffunlem  34387  satffunlem1lem2  34389  satffunlem2lem1  34390  satffunlem2lem2  34392  msrval  34524  msrf  34528  ismfs  34535  clsun  35208  poimirlem8  36491  itg2addnclem2  36535  heiborlem4  36677  heiborlem6  36679  heiborlem10  36683  pmodl42N  38717  polfvalN  38770  poldmj1N  38794  pmapj2N  38795  pnonsingN  38799  psubclinN  38814  poml4N  38819  osumcllem9N  38830  trnfsetN  39021  diainN  39923  djaffvalN  39999  djafvalN  40000  djajN  40003  dihmeetcl  40211  dihmeet2  40212  dochnoncon  40257  djhffval  40262  djhfval  40263  djhlj  40267  dochdmm1  40276  lclkrlem2g  40379  lclkrlem2v  40394  lcfrlem21  40429  lcfrlem24  40432  mapdunirnN  40516  baerlem5amN  40582  baerlem5bmN  40583  baerlem5abmN  40584  mapdheq4lem  40597  mapdh6lem1N  40599  mapdh6lem2N  40600  hdmap1l6lem1  40673  hdmap1l6lem2  40674  aomclem8  41793  disjrnmpt2  43876  dvsinax  44619  dvcosax  44632  nnfoctbdjlem  45161  smfpimcc  45514  smfsuplem2  45518  rhmval  46712  iscnrm3l  47574