Theorem ineq12d 4182

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

Syntax hints:   → wi 4   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  csbin  4405  predeq123  6300  funcnvtp  6596  fnunres1  6645  ofrfvalg  7680  offval  7681  oev2  8504  isf32lem7  10339  ressval  17289  invffval  17811  invfval  17812  dfiso2  17825  isofn  17828  oppcinv  17833  zerooval  18048  cat1  18150  isps  18620  dmdprd  20066  dprddisj  20077  dprdf1o  20100  dmdprdsplit2lem  20113  dmdprdpr  20117  pgpfaclem1  20149  isunit  20451  dfrhm2  20552  isrhm  20556  rhmval  20578  2idlval  21357  pjfval  21821  aspval  21987  ressmplbas2  22142  isconn  23535  connsuba  23542  ptbasin  23699  ptclsg  23737  qtopval  23817  rnelfmlem  24074  trust  24351  isnmhm  24868  uniioombllem2a  25706  dyaddisjlem  25719  dyaddisj  25720  i1faddlem  25817  i1fmullem  25818  limcflf  26005  ewlksfval  29888  isewlk  29889  ewlkinedg  29891  ispth  30007  trlsegvdeg  30515  frcond3  30557  numclwwlk3lem2  30672  chocin  31784  cmbr3  31897  pjoml3  31901  fh1  31907  xppreima2  32933  cosnopne  32976  swrdrndisj  33214  hauseqcn  34229  prsssdm  34248  ordtrestNEW  34252  ordtrest2NEW  34254  cndprobval  34764  ballotlemfrc  34858  bnj1421  35371  satffunlem  35788  satffunlem1lem2  35790  satffunlem2lem1  35791  satffunlem2lem2  35793  msrval  35925  msrf  35929  ismfs  35936  clsun  36724  poimirlem8  38162  itg2addnclem2  38206  heiborlem4  38348  heiborlem6  38350  heiborlem10  38354  shiftstableeq2  39017  pmodl42N  40510  polfvalN  40563  poldmj1N  40587  pmapj2N  40588  pnonsingN  40592  psubclinN  40607  poml4N  40612  osumcllem9N  40623  trnfsetN  40814  diainN  41716  djaffvalN  41792  djafvalN  41793  djajN  41796  dihmeetcl  42004  dihmeet2  42005  dochnoncon  42050  djhffval  42055  djhfval  42056  djhlj  42060  dochdmm1  42069  lclkrlem2g  42172  lclkrlem2v  42187  lcfrlem21  42222  lcfrlem24  42225  mapdunirnN  42309  baerlem5amN  42375  baerlem5bmN  42376  baerlem5abmN  42377  mapdheq4lem  42390  mapdh6lem1N  42392  mapdh6lem2N  42393  hdmap1l6lem1  42466  hdmap1l6lem2  42467  aomclem8  43673  disjrnmpt2  45791  dvsinax  46512  dvcosax  46525  nnfoctbdjlem  47054  smfpimcc  47407  smfsuplem2  47411  upgrimpths  48556  iscnrm3l  49607  invfn  49686  invpropdlem  49694  infsubc2d  49718  zeroopropdlem  49898  zeroopropd  49901