Theorem ineq12d 4213

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-in 3955

This theorem is referenced by:  csbin  4439  predeq123  6301  funcnvtp  6611  fnunres1  6661  ofrfvalg  7682  offval  7683  oev2  8529  isf32lem7  10360  ressval  17183  invffval  17712  invfval  17713  dfiso2  17726  isofn  17729  oppcinv  17734  zerooval  17955  cat1  18057  isps  18531  dmdprd  19916  dprddisj  19927  dprdf1o  19950  dmdprdsplit2lem  19963  dmdprdpr  19967  pgpfaclem1  19999  isunit  20271  dfrhm2  20372  isrhm  20376  rhmval  20398  2idlval  21096  pjfval  21571  aspval  21737  ressmplbas2  21893  isconn  23237  connsuba  23244  ptbasin  23401  ptclsg  23439  qtopval  23519  rnelfmlem  23776  trust  24054  isnmhm  24583  uniioombllem2a  25431  dyaddisjlem  25444  dyaddisj  25445  i1faddlem  25542  i1fmullem  25543  limcflf  25730  ewlksfval  29292  isewlk  29293  ewlkinedg  29295  ispth  29414  trlsegvdeg  29914  frcond3  29956  numclwwlk3lem2  30071  chocin  31182  cmbr3  31295  pjoml3  31299  fh1  31305  xppreima2  32310  cosnopne  32350  swrdrndisj  32555  hauseqcn  33343  prsssdm  33362  ordtrestNEW  33366  ordtrest2NEW  33368  cndprobval  33897  ballotlemfrc  33990  bnj1421  34518  satffunlem  34857  satffunlem1lem2  34859  satffunlem2lem1  34860  satffunlem2lem2  34862  msrval  34994  msrf  34998  ismfs  35005  clsun  35679  poimirlem8  36962  itg2addnclem2  37006  heiborlem4  37148  heiborlem6  37150  heiborlem10  37154  pmodl42N  39188  polfvalN  39241  poldmj1N  39265  pmapj2N  39266  pnonsingN  39270  psubclinN  39285  poml4N  39290  osumcllem9N  39301  trnfsetN  39492  diainN  40394  djaffvalN  40470  djafvalN  40471  djajN  40474  dihmeetcl  40682  dihmeet2  40683  dochnoncon  40728  djhffval  40733  djhfval  40734  djhlj  40738  dochdmm1  40747  lclkrlem2g  40850  lclkrlem2v  40865  lcfrlem21  40900  lcfrlem24  40903  mapdunirnN  40987  baerlem5amN  41053  baerlem5bmN  41054  baerlem5abmN  41055  mapdheq4lem  41068  mapdh6lem1N  41070  mapdh6lem2N  41071  hdmap1l6lem1  41144  hdmap1l6lem2  41145  aomclem8  42268  disjrnmpt2  44348  dvsinax  45090  dvcosax  45103  nnfoctbdjlem  45632  smfpimcc  45985  smfsuplem2  45989  iscnrm3l  47748