Theorem ineq12d 4228

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

Syntax hints:   → wi 4   = wceq 1536   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969

This theorem is referenced by:  csbin  4447  predeq123  6323  funcnvtp  6630  fnunres1  6680  ofrfvalg  7704  offval  7705  oev2  8559  isf32lem7  10396  ressval  17276  invffval  17805  invfval  17806  dfiso2  17819  isofn  17822  oppcinv  17827  zerooval  18048  cat1  18150  isps  18625  dmdprd  20032  dprddisj  20043  dprdf1o  20066  dmdprdsplit2lem  20079  dmdprdpr  20083  pgpfaclem1  20115  isunit  20389  dfrhm2  20490  isrhm  20494  rhmval  20516  2idlval  21278  pjfval  21743  aspval  21910  ressmplbas2  22062  isconn  23436  connsuba  23443  ptbasin  23600  ptclsg  23638  qtopval  23718  rnelfmlem  23975  trust  24253  isnmhm  24782  uniioombllem2a  25630  dyaddisjlem  25643  dyaddisj  25644  i1faddlem  25741  i1fmullem  25742  limcflf  25930  ewlksfval  29633  isewlk  29634  ewlkinedg  29636  ispth  29755  trlsegvdeg  30255  frcond3  30297  numclwwlk3lem2  30412  chocin  31523  cmbr3  31636  pjoml3  31640  fh1  31646  xppreima2  32667  cosnopne  32708  swrdrndisj  32926  hauseqcn  33858  prsssdm  33877  ordtrestNEW  33881  ordtrest2NEW  33883  cndprobval  34414  ballotlemfrc  34507  bnj1421  35034  satffunlem  35385  satffunlem1lem2  35387  satffunlem2lem1  35388  satffunlem2lem2  35390  msrval  35522  msrf  35526  ismfs  35533  clsun  36310  poimirlem8  37614  itg2addnclem2  37658  heiborlem4  37800  heiborlem6  37802  heiborlem10  37806  pmodl42N  39833  polfvalN  39886  poldmj1N  39910  pmapj2N  39911  pnonsingN  39915  psubclinN  39930  poml4N  39935  osumcllem9N  39946  trnfsetN  40137  diainN  41039  djaffvalN  41115  djafvalN  41116  djajN  41119  dihmeetcl  41327  dihmeet2  41328  dochnoncon  41373  djhffval  41378  djhfval  41379  djhlj  41383  dochdmm1  41392  lclkrlem2g  41495  lclkrlem2v  41510  lcfrlem21  41545  lcfrlem24  41548  mapdunirnN  41632  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdheq4lem  41713  mapdh6lem1N  41715  mapdh6lem2N  41716  hdmap1l6lem1  41789  hdmap1l6lem2  41790  aomclem8  43049  disjrnmpt2  45130  dvsinax  45868  dvcosax  45881  nnfoctbdjlem  46410  smfpimcc  46763  smfsuplem2  46767  iscnrm3l  48747