Theorem ineq12d 4187

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924

This theorem is referenced by:  csbin  4408  predeq123  6278  funcnvtp  6582  fnunres1  6633  ofrfvalg  7664  offval  7665  oev2  8490  isf32lem7  10319  ressval  17210  invffval  17727  invfval  17728  dfiso2  17741  isofn  17744  oppcinv  17749  zerooval  17964  cat1  18066  isps  18534  dmdprd  19937  dprddisj  19948  dprdf1o  19971  dmdprdsplit2lem  19984  dmdprdpr  19988  pgpfaclem1  20020  isunit  20289  dfrhm2  20390  isrhm  20394  rhmval  20416  2idlval  21168  pjfval  21622  aspval  21789  ressmplbas2  21941  isconn  23307  connsuba  23314  ptbasin  23471  ptclsg  23509  qtopval  23589  rnelfmlem  23846  trust  24124  isnmhm  24641  uniioombllem2a  25490  dyaddisjlem  25503  dyaddisj  25504  i1faddlem  25601  i1fmullem  25602  limcflf  25789  ewlksfval  29536  isewlk  29537  ewlkinedg  29539  ispth  29658  trlsegvdeg  30163  frcond3  30205  numclwwlk3lem2  30320  chocin  31431  cmbr3  31544  pjoml3  31548  fh1  31554  xppreima2  32582  cosnopne  32624  swrdrndisj  32886  hauseqcn  33895  prsssdm  33914  ordtrestNEW  33918  ordtrest2NEW  33920  cndprobval  34431  ballotlemfrc  34525  bnj1421  35039  satffunlem  35395  satffunlem1lem2  35397  satffunlem2lem1  35398  satffunlem2lem2  35400  msrval  35532  msrf  35536  ismfs  35543  clsun  36323  poimirlem8  37629  itg2addnclem2  37673  heiborlem4  37815  heiborlem6  37817  heiborlem10  37821  pmodl42N  39852  polfvalN  39905  poldmj1N  39929  pmapj2N  39930  pnonsingN  39934  psubclinN  39949  poml4N  39954  osumcllem9N  39965  trnfsetN  40156  diainN  41058  djaffvalN  41134  djafvalN  41135  djajN  41138  dihmeetcl  41346  dihmeet2  41347  dochnoncon  41392  djhffval  41397  djhfval  41398  djhlj  41402  dochdmm1  41411  lclkrlem2g  41514  lclkrlem2v  41529  lcfrlem21  41564  lcfrlem24  41567  mapdunirnN  41651  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdheq4lem  41732  mapdh6lem1N  41734  mapdh6lem2N  41735  hdmap1l6lem1  41808  hdmap1l6lem2  41809  aomclem8  43057  disjrnmpt2  45189  dvsinax  45918  dvcosax  45931  nnfoctbdjlem  46460  smfpimcc  46813  smfsuplem2  46817  upgrimpths  47913  iscnrm3l  48943  invfn  49023  invpropdlem  49031  infsubc2d  49055  zeroopropdlem  49235  zeroopropd  49238