Theorem ineq12d 4167

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  csbin  4400  predeq123  6304  funcnvtp  6601  fnunres1  6649  ofrfvalg  7699  offval  7700  oev2  8524  isf32lem7  10430  ressval  17404  invffval  17926  invfval  17927  dfiso2  17940  isofn  17943  oppcinv  17948  zerooval  18163  cat1  18265  isps  18735  dmdprd  20207  dprddisj  20218  dprdf1o  20241  dmdprdsplit2lem  20254  dmdprdpr  20258  pgpfaclem1  20290  isunit  20596  dfrhm2  20697  isrhm  20702  rhmval  20731  2idlval  21537  pjfval  22005  aspval  22173  ressmplbas2  22328  isconn  23724  connsuba  23731  ptbasin  23889  ptclsg  23927  qtopval  24007  rnelfmlem  24264  trust  24541  isnmhm  25058  uniioombllem2a  25896  dyaddisjlem  25909  dyaddisj  25910  i1faddlem  26007  i1fmullem  26008  limcflf  26194  angmgmaddov1  29381  angmgmval  29387  prlngsymquadlem  29434  ewlksfval  30175  isewlk  30176  ewlkinedg  30178  ispth  30299  trlsegvdeg  30821  frcond3  30863  numclwwlk3lem2  30978  chocin  32090  cmbr3  32203  pjoml3  32207  fh1  32213  xppreima2  33238  cosnopne  33280  swrdrndisj  33511  hauseqcn  34523  prsssdm  34542  ordtrestNEW  34546  ordtrest2NEW  34548  cndprobval  35058  ballotlemfrc  35152  bnj1421  35665  satffunlem  36145  satffunlem1lem2  36147  satffunlem2lem1  36148  satffunlem2lem2  36150  msrval  36282  msrf  36286  ismfs  36293  clsun  37096  poimirlem8  38526  itg2addnclem2  38570  heiborlem4  38728  heiborlem6  38730  heiborlem10  38734  shiftstableeq2  39395  pmodl42N  40888  polfvalN  40941  poldmj1N  40965  pmapj2N  40966  pnonsingN  40970  psubclinN  40985  poml4N  40990  osumcllem9N  41001  trnfsetN  41192  diainN  42094  djaffvalN  42170  djafvalN  42171  djajN  42174  dihmeetcl  42382  dihmeet2  42383  dochnoncon  42428  djhffval  42433  djhfval  42434  djhlj  42438  dochdmm1  42447  lclkrlem2g  42550  lclkrlem2v  42565  lcfrlem21  42600  lcfrlem24  42603  mapdunirnN  42687  baerlem5amN  42753  baerlem5bmN  42754  baerlem5abmN  42755  mapdheq4lem  42768  mapdh6lem1N  42770  mapdh6lem2N  42771  hdmap1l6lem1  42844  hdmap1l6lem2  42845  aomclem8  44047  disjrnmpt2  46172  dvsinax  46892  dvcosax  46905  nnfoctbdjlem  47434  smfpimcc  47787  smfsuplem2  47791  upgrimpths  48976  iscnrm3l  50028  invfn  50107  invpropdlem  50115  infsubc2d  50139  zeroopropdlem  50319  zeroopropd  50322