Theorem ineq12d 4184

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921

This theorem is referenced by:  csbin  4405  predeq123  6275  funcnvtp  6579  fnunres1  6630  ofrfvalg  7661  offval  7662  oev2  8487  isf32lem7  10312  ressval  17203  invffval  17720  invfval  17721  dfiso2  17734  isofn  17737  oppcinv  17742  zerooval  17957  cat1  18059  isps  18527  dmdprd  19930  dprddisj  19941  dprdf1o  19964  dmdprdsplit2lem  19977  dmdprdpr  19981  pgpfaclem1  20013  isunit  20282  dfrhm2  20383  isrhm  20387  rhmval  20409  2idlval  21161  pjfval  21615  aspval  21782  ressmplbas2  21934  isconn  23300  connsuba  23307  ptbasin  23464  ptclsg  23502  qtopval  23582  rnelfmlem  23839  trust  24117  isnmhm  24634  uniioombllem2a  25483  dyaddisjlem  25496  dyaddisj  25497  i1faddlem  25594  i1fmullem  25595  limcflf  25782  ewlksfval  29529  isewlk  29530  ewlkinedg  29532  ispth  29651  trlsegvdeg  30156  frcond3  30198  numclwwlk3lem2  30313  chocin  31424  cmbr3  31537  pjoml3  31541  fh1  31547  xppreima2  32575  cosnopne  32617  swrdrndisj  32879  hauseqcn  33888  prsssdm  33907  ordtrestNEW  33911  ordtrest2NEW  33913  cndprobval  34424  ballotlemfrc  34518  bnj1421  35032  satffunlem  35388  satffunlem1lem2  35390  satffunlem2lem1  35391  satffunlem2lem2  35393  msrval  35525  msrf  35529  ismfs  35536  clsun  36316  poimirlem8  37622  itg2addnclem2  37666  heiborlem4  37808  heiborlem6  37810  heiborlem10  37814  pmodl42N  39845  polfvalN  39898  poldmj1N  39922  pmapj2N  39923  pnonsingN  39927  psubclinN  39942  poml4N  39947  osumcllem9N  39958  trnfsetN  40149  diainN  41051  djaffvalN  41127  djafvalN  41128  djajN  41131  dihmeetcl  41339  dihmeet2  41340  dochnoncon  41385  djhffval  41390  djhfval  41391  djhlj  41395  dochdmm1  41404  lclkrlem2g  41507  lclkrlem2v  41522  lcfrlem21  41557  lcfrlem24  41560  mapdunirnN  41644  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdheq4lem  41725  mapdh6lem1N  41727  mapdh6lem2N  41728  hdmap1l6lem1  41801  hdmap1l6lem2  41802  aomclem8  43050  disjrnmpt2  45182  dvsinax  45911  dvcosax  45924  nnfoctbdjlem  46453  smfpimcc  46806  smfsuplem2  46810  upgrimpths  47909  iscnrm3l  48939  invfn  49019  invpropdlem  49027  infsubc2d  49051  zeroopropdlem  49231  zeroopropd  49234