Theorem ineq12d 4175

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

Syntax hints:   → wi 4   = wceq 1570   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913

This theorem is referenced by:  csbin  4408  predeq123  6305  funcnvtp  6601  fnunres1  6649  ofrfvalg  7684  offval  7685  oev2  8509  isf32lem7  10344  ressval  17294  invffval  17816  invfval  17817  dfiso2  17830  isofn  17833  oppcinv  17838  zerooval  18053  cat1  18155  isps  18625  dmdprd  20071  dprddisj  20082  dprdf1o  20105  dmdprdsplit2lem  20118  dmdprdpr  20122  pgpfaclem1  20154  isunit  20456  dfrhm2  20557  isrhm  20561  rhmval  20583  2idlval  21371  pjfval  21837  aspval  22003  ressmplbas2  22158  isconn  23551  connsuba  23558  ptbasin  23715  ptclsg  23753  qtopval  23833  rnelfmlem  24090  trust  24367  isnmhm  24884  uniioombllem2a  25722  dyaddisjlem  25735  dyaddisj  25736  i1faddlem  25833  i1fmullem  25834  limcflf  26021  prlngsymquadlem  29194  ewlksfval  29932  isewlk  29933  ewlkinedg  29935  ispth  30051  trlsegvdeg  30559  frcond3  30601  numclwwlk3lem2  30716  chocin  31828  cmbr3  31941  pjoml3  31945  fh1  31951  xppreima2  32977  cosnopne  33020  swrdrndisj  33258  hauseqcn  34269  prsssdm  34288  ordtrestNEW  34292  ordtrest2NEW  34294  cndprobval  34804  ballotlemfrc  34898  bnj1421  35411  satffunlem  35874  satffunlem1lem2  35876  satffunlem2lem1  35877  satffunlem2lem2  35879  msrval  36011  msrf  36015  ismfs  36022  clsun  36820  poimirlem8  38260  itg2addnclem2  38304  heiborlem4  38446  heiborlem6  38448  heiborlem10  38452  shiftstableeq2  39113  pmodl42N  40606  polfvalN  40659  poldmj1N  40683  pmapj2N  40684  pnonsingN  40688  psubclinN  40703  poml4N  40708  osumcllem9N  40719  trnfsetN  40910  diainN  41812  djaffvalN  41888  djafvalN  41889  djajN  41892  dihmeetcl  42100  dihmeet2  42101  dochnoncon  42146  djhffval  42151  djhfval  42152  djhlj  42156  dochdmm1  42165  lclkrlem2g  42268  lclkrlem2v  42283  lcfrlem21  42318  lcfrlem24  42321  mapdunirnN  42405  baerlem5amN  42471  baerlem5bmN  42472  baerlem5abmN  42473  mapdheq4lem  42486  mapdh6lem1N  42488  mapdh6lem2N  42489  hdmap1l6lem1  42562  hdmap1l6lem2  42563  aomclem8  43771  disjrnmpt2  45889  dvsinax  46610  dvcosax  46623  nnfoctbdjlem  47152  smfpimcc  47505  smfsuplem2  47509  upgrimpths  48657  iscnrm3l  49712  invfn  49791  invpropdlem  49799  infsubc2d  49823  zeroopropdlem  50003  zeroopropd  50006