Theorem ineq12d 4121

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  csbin  4403  predeq123  6331  funcnvtp  6633  fnunres1  6681  ofrfvalg  7733  offval  7734  oev2  8569  isf32lem7  10476  ressval  17455  invffval  17983  invfval  17984  dfiso2  17997  isofn  18000  oppcinv  18005  zerooval  18220  cat1  18322  isps  18792  dmdprd  20265  dprddisj  20276  dprdf1o  20299  dmdprdsplit2lem  20312  dmdprdpr  20316  pgpfaclem1  20348  isunit  20654  dfrhm2  20755  isrhm  20760  rhmval  20789  2idlval  21595  pjfval  22067  aspval  22235  ressmplbas2  22390  isconn  23786  connsuba  23793  ptbasin  23951  ptclsg  23989  qtopval  24069  rnelfmlem  24326  trust  24603  isnmhm  25120  uniioombllem2a  25958  dyaddisjlem  25971  dyaddisj  25972  i1faddlem  26069  i1fmullem  26070  limcflf  26256  angmgmaddov1  29445  angmgmval  29451  prlngsymquadlem  29498  ewlksfval  30239  isewlk  30240  ewlkinedg  30242  ispth  30363  trlsegvdeg  30885  frcond3  30927  numclwwlk3lem2  31042  chocin  32154  cmbr3  32267  pjoml3  32271  fh1  32277  xppreima2  33343  cosnopne  33384  swrdrndisj  33614  hauseqcn  34641  prsssdm  34660  ordtrestNEW  34664  ordtrest2NEW  34666  cndprobval  35176  ballotlemfrc  35270  bnj1421  35783  satffunlem  36374  satffunlem1lem2  36376  satffunlem2lem1  36377  satffunlem2lem2  36379  msrval  36511  msrf  36515  ismfs  36522  clsun  37331  poimirlem8  38814  itg2addnclem2  38858  heiborlem4  39014  heiborlem6  39016  heiborlem10  39020  shiftstableeq2  39681  pmodl42N  41174  polfvalN  41227  poldmj1N  41251  pmapj2N  41252  pnonsingN  41256  psubclinN  41271  poml4N  41276  osumcllem9N  41287  trnfsetN  41478  diainN  42380  djaffvalN  42456  djafvalN  42457  djajN  42460  dihmeetcl  42668  dihmeet2  42669  dochnoncon  42714  djhffval  42719  djhfval  42720  djhlj  42724  dochdmm1  42733  lclkrlem2g  42836  lclkrlem2v  42851  lcfrlem21  42886  lcfrlem24  42889  mapdunirnN  42973  baerlem5amN  43039  baerlem5bmN  43040  baerlem5abmN  43041  mapdheq4lem  43054  mapdh6lem1N  43056  mapdh6lem2N  43057  hdmap1l6lem1  43130  hdmap1l6lem2  43131  aomclem8  44329  disjrnmpt2  46476  dvsinax  47196  dvcosax  47209  nnfoctbdjlem  47738  smfpimcc  48091  smfsuplem2  48095  upgrimpths  49280  iscnrm3l  50396  invfn  50475  invpropdlem  50483  infsubc2d  50507  zeroopropdlem  50695  zeroopropd  50698  parcoval  51093