Theorem ineq12d 4214

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  csbin  4440  predeq123  6302  funcnvtp  6612  fnunres1  6662  ofrfvalg  7678  offval  7679  oev2  8523  isf32lem7  10354  ressval  17176  invffval  17705  invfval  17706  dfiso2  17719  isofn  17722  oppcinv  17727  zerooval  17945  cat1  18047  isps  18521  dmdprd  19868  dprddisj  19879  dprdf1o  19902  dmdprdsplit2lem  19915  dmdprdpr  19919  pgpfaclem1  19951  isunit  20187  dfrhm2  20253  isrhm  20257  2idlval  20858  pjfval  21261  aspval  21427  ressmplbas2  21582  isconn  22917  connsuba  22924  ptbasin  23081  ptclsg  23119  qtopval  23199  rnelfmlem  23456  trust  23734  isnmhm  24263  uniioombllem2a  25099  dyaddisjlem  25112  dyaddisj  25113  i1faddlem  25210  i1fmullem  25211  limcflf  25398  ewlksfval  28858  isewlk  28859  ewlkinedg  28861  ispth  28980  trlsegvdeg  29480  frcond3  29522  numclwwlk3lem2  29637  chocin  30748  cmbr3  30861  pjoml3  30865  fh1  30871  xppreima2  31876  cosnopne  31916  swrdrndisj  32121  hauseqcn  32878  prsssdm  32897  ordtrestNEW  32901  ordtrest2NEW  32903  cndprobval  33432  ballotlemfrc  33525  bnj1421  34053  satffunlem  34392  satffunlem1lem2  34394  satffunlem2lem1  34395  satffunlem2lem2  34397  msrval  34529  msrf  34533  ismfs  34540  clsun  35213  poimirlem8  36496  itg2addnclem2  36540  heiborlem4  36682  heiborlem6  36684  heiborlem10  36688  pmodl42N  38722  polfvalN  38775  poldmj1N  38799  pmapj2N  38800  pnonsingN  38804  psubclinN  38819  poml4N  38824  osumcllem9N  38835  trnfsetN  39026  diainN  39928  djaffvalN  40004  djafvalN  40005  djajN  40008  dihmeetcl  40216  dihmeet2  40217  dochnoncon  40262  djhffval  40267  djhfval  40268  djhlj  40272  dochdmm1  40281  lclkrlem2g  40384  lclkrlem2v  40399  lcfrlem21  40434  lcfrlem24  40437  mapdunirnN  40521  baerlem5amN  40587  baerlem5bmN  40588  baerlem5abmN  40589  mapdheq4lem  40602  mapdh6lem1N  40604  mapdh6lem2N  40605  hdmap1l6lem1  40678  hdmap1l6lem2  40679  aomclem8  41803  disjrnmpt2  43886  dvsinax  44629  dvcosax  44642  nnfoctbdjlem  45171  smfpimcc  45524  smfsuplem2  45528  rhmval  46722  iscnrm3l  47584