Theorem ineq12d 4196

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933

This theorem is referenced by:  csbin  4417  predeq123  6291  funcnvtp  6598  fnunres1  6649  ofrfvalg  7677  offval  7678  oev2  8533  isf32lem7  10371  ressval  17252  invffval  17769  invfval  17770  dfiso2  17783  isofn  17786  oppcinv  17791  zerooval  18006  cat1  18108  isps  18576  dmdprd  19979  dprddisj  19990  dprdf1o  20013  dmdprdsplit2lem  20026  dmdprdpr  20030  pgpfaclem1  20062  isunit  20331  dfrhm2  20432  isrhm  20436  rhmval  20458  2idlval  21210  pjfval  21664  aspval  21831  ressmplbas2  21983  isconn  23349  connsuba  23356  ptbasin  23513  ptclsg  23551  qtopval  23631  rnelfmlem  23888  trust  24166  isnmhm  24683  uniioombllem2a  25533  dyaddisjlem  25546  dyaddisj  25547  i1faddlem  25644  i1fmullem  25645  limcflf  25832  ewlksfval  29527  isewlk  29528  ewlkinedg  29530  ispth  29649  trlsegvdeg  30154  frcond3  30196  numclwwlk3lem2  30311  chocin  31422  cmbr3  31535  pjoml3  31539  fh1  31545  xppreima2  32575  cosnopne  32617  swrdrndisj  32879  hauseqcn  33875  prsssdm  33894  ordtrestNEW  33898  ordtrest2NEW  33900  cndprobval  34411  ballotlemfrc  34505  bnj1421  35019  satffunlem  35369  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  msrval  35506  msrf  35510  ismfs  35517  clsun  36292  poimirlem8  37598  itg2addnclem2  37642  heiborlem4  37784  heiborlem6  37786  heiborlem10  37790  pmodl42N  39816  polfvalN  39869  poldmj1N  39893  pmapj2N  39894  pnonsingN  39898  psubclinN  39913  poml4N  39918  osumcllem9N  39929  trnfsetN  40120  diainN  41022  djaffvalN  41098  djafvalN  41099  djajN  41102  dihmeetcl  41310  dihmeet2  41311  dochnoncon  41356  djhffval  41361  djhfval  41362  djhlj  41366  dochdmm1  41375  lclkrlem2g  41478  lclkrlem2v  41493  lcfrlem21  41528  lcfrlem24  41531  mapdunirnN  41615  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdheq4lem  41696  mapdh6lem1N  41698  mapdh6lem2N  41699  hdmap1l6lem1  41772  hdmap1l6lem2  41773  aomclem8  43032  disjrnmpt2  45160  dvsinax  45890  dvcosax  45903  nnfoctbdjlem  46432  smfpimcc  46785  smfsuplem2  46789  upgrimpths  47870  iscnrm3l  48873  invfn  48948  invpropdlem  48953  infsubc2d  48977  zeroopropdlem  49107  zeroopropd  49110