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  28889  isewlk  28890  ewlkinedg  28892  ispth  29011  trlsegvdeg  29511  frcond3  29553  numclwwlk3lem2  29668  chocin  30779  cmbr3  30892  pjoml3  30896  fh1  30902  xppreima2  31907  cosnopne  31947  swrdrndisj  32152  hauseqcn  32909  prsssdm  32928  ordtrestNEW  32932  ordtrest2NEW  32934  cndprobval  33463  ballotlemfrc  33556  bnj1421  34084  satffunlem  34423  satffunlem1lem2  34425  satffunlem2lem1  34426  satffunlem2lem2  34428  msrval  34560  msrf  34564  ismfs  34571  clsun  35261  poimirlem8  36544  itg2addnclem2  36588  heiborlem4  36730  heiborlem6  36732  heiborlem10  36736  pmodl42N  38770  polfvalN  38823  poldmj1N  38847  pmapj2N  38848  pnonsingN  38852  psubclinN  38867  poml4N  38872  osumcllem9N  38883  trnfsetN  39074  diainN  39976  djaffvalN  40052  djafvalN  40053  djajN  40056  dihmeetcl  40264  dihmeet2  40265  dochnoncon  40310  djhffval  40315  djhfval  40316  djhlj  40320  dochdmm1  40329  lclkrlem2g  40432  lclkrlem2v  40447  lcfrlem21  40482  lcfrlem24  40485  mapdunirnN  40569  baerlem5amN  40635  baerlem5bmN  40636  baerlem5abmN  40637  mapdheq4lem  40650  mapdh6lem1N  40652  mapdh6lem2N  40653  hdmap1l6lem1  40726  hdmap1l6lem2  40727  aomclem8  41851  disjrnmpt2  43934  dvsinax  44677  dvcosax  44690  nnfoctbdjlem  45219  smfpimcc  45572  smfsuplem2  45576  rhmval  46770  iscnrm3l  47632