Theorem ineq12d 4171

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

Syntax hints:   → wi 4   = wceq 1559   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3909

This theorem is referenced by:  csbin  4393  predeq123  6284  funcnvtp  6579  fnunres1  6628  ofrfvalg  7663  offval  7664  oev2  8486  isf32lem7  10310  ressval  17260  invffval  17782  invfval  17783  dfiso2  17796  isofn  17799  oppcinv  17804  zerooval  18019  cat1  18121  isps  18591  dmdprd  20031  dprddisj  20042  dprdf1o  20065  dmdprdsplit2lem  20078  dmdprdpr  20082  pgpfaclem1  20114  isunit  20409  dfrhm2  20510  isrhm  20514  rhmval  20536  2idlval  21309  pjfval  21746  aspval  21912  ressmplbas2  22067  isconn  23461  connsuba  23468  ptbasin  23625  ptclsg  23663  qtopval  23743  rnelfmlem  24000  trust  24277  isnmhm  24794  uniioombllem2a  25632  dyaddisjlem  25645  dyaddisj  25646  i1faddlem  25743  i1fmullem  25744  limcflf  25931  ewlksfval  29759  isewlk  29760  ewlkinedg  29762  ispth  29878  trlsegvdeg  30386  frcond3  30428  numclwwlk3lem2  30543  chocin  31655  cmbr3  31768  pjoml3  31772  fh1  31778  xppreima2  32814  cosnopne  32857  swrdrndisj  33096  hauseqcn  34156  prsssdm  34175  ordtrestNEW  34179  ordtrest2NEW  34181  cndprobval  34691  ballotlemfrc  34785  bnj1421  35298  satffunlem  35712  satffunlem1lem2  35714  satffunlem2lem1  35715  satffunlem2lem2  35717  msrval  35849  msrf  35853  ismfs  35860  clsun  36649  poimirlem8  38088  itg2addnclem2  38132  heiborlem4  38274  heiborlem6  38276  heiborlem10  38280  shiftstableeq2  38943  pmodl42N  40436  polfvalN  40489  poldmj1N  40513  pmapj2N  40514  pnonsingN  40518  psubclinN  40533  poml4N  40538  osumcllem9N  40549  trnfsetN  40740  diainN  41642  djaffvalN  41718  djafvalN  41719  djajN  41722  dihmeetcl  41930  dihmeet2  41931  dochnoncon  41976  djhffval  41981  djhfval  41982  djhlj  41986  dochdmm1  41995  lclkrlem2g  42098  lclkrlem2v  42113  lcfrlem21  42148  lcfrlem24  42151  mapdunirnN  42235  baerlem5amN  42301  baerlem5bmN  42302  baerlem5abmN  42303  mapdheq4lem  42316  mapdh6lem1N  42318  mapdh6lem2N  42319  hdmap1l6lem1  42392  hdmap1l6lem2  42393  aomclem8  43599  disjrnmpt2  45727  dvsinax  46448  dvcosax  46461  nnfoctbdjlem  46990  smfpimcc  47343  smfsuplem2  47347  upgrimpths  48492  iscnrm3l  49533  invfn  49612  invpropdlem  49620  infsubc2d  49644  zeroopropdlem  49824  zeroopropd  49827