Theorem ineq12d 3777

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

Syntax hints:   → wi 4   = wceq 1475   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  csbin  3962  predeq123  5598  funprgOLD  5855  funtpgOLD  5857  funcnvtp  5865  offval  6802  ofrfval  6803  oev2  7490  isf32lem7  9064  ressval  15754  invffval  16241  invfval  16242  dfiso2  16255  isofn  16258  oppcinv  16263  zerooval  16472  isps  17025  dmdprd  18220  dprddisj  18231  dprdf1o  18254  dmdprdsplit2lem  18267  dmdprdpr  18271  pgpfaclem1  18303  isunit  18480  dfrhm2  18540  isrhm  18544  2idlval  19054  aspval  19149  ressmplbas2  19276  pjfval  19869  iscon  21026  consuba  21033  ptbasin  21190  ptclsg  21228  qtopval  21308  rnelfmlem  21566  trust  21843  isnmhm  22360  uniioombllem2a  23156  dyaddisjlem  23169  dyaddisj  23170  i1faddlem  23266  i1fmullem  23267  limcflf  23451  ispth  26098  1pthonlem2  26120  2pthlem2  26126  constr2pth  26131  constr3pthlem3  26185  frisusgranb  26524  2spotdisj  26588  chocin  27738  cmbr3  27851  pjoml3  27855  fh1  27861  xppreima2  28830  hauseqcn  29269  prsssdm  29291  ordtrestNEW  29295  ordtrest2NEW  29297  cndprobval  29822  ballotlemfrc  29915  bnj1421  30364  msrval  30689  msrf  30693  ismfs  30700  clsun  31493  poimirlem8  32587  itg2addnclem2  32632  heiborlem4  32783  heiborlem6  32785  heiborlem10  32789  pmodl42N  34155  polfvalN  34208  poldmj1N  34232  pmapj2N  34233  pnonsingN  34237  psubclinN  34252  poml4N  34257  osumcllem9N  34268  trnfsetN  34460  diainN  35364  djaffvalN  35440  djafvalN  35441  djajN  35444  dihmeetcl  35652  dihmeet2  35653  dochnoncon  35698  djhffval  35703  djhfval  35704  djhlj  35708  dochdmm1  35717  lclkrlem2g  35820  lclkrlem2v  35835  lcfrlem21  35870  lcfrlem24  35873  mapdunirnN  35957  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdheq4lem  36038  mapdh6lem1N  36040  mapdh6lem2N  36041  hdmap1l6lem1  36115  hdmap1l6lem2  36116  aomclem8  36649  csbingOLD  38076  disjrnmpt2  38370  dvsinax  38801  dvcosax  38816  nnfoctbdjlem  39348  ewlksfval  40803  isewlk  40804  ewlkinedg  40806  isPth  40929  trlsegvdeg  41395  frcond3  41440  rhmval  41709