Theorem ineq12d 4174

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  csbin  4407  predeq123  6307  funcnvtp  6603  fnunres1  6651  ofrfvalg  7688  offval  7689  oev2  8510  isf32lem7  10354  ressval  17311  invffval  17833  invfval  17834  dfiso2  17847  isofn  17850  oppcinv  17855  zerooval  18070  cat1  18172  isps  18642  dmdprd  20094  dprddisj  20105  dprdf1o  20128  dmdprdsplit2lem  20141  dmdprdpr  20145  pgpfaclem1  20177  isunit  20481  dfrhm2  20582  isrhm  20587  rhmval  20616  2idlval  21420  pjfval  21886  aspval  22052  ressmplbas2  22207  isconn  23600  connsuba  23607  ptbasin  23765  ptclsg  23803  qtopval  23883  rnelfmlem  24140  trust  24417  isnmhm  24934  uniioombllem2a  25772  dyaddisjlem  25785  dyaddisj  25786  i1faddlem  25883  i1fmullem  25884  limcflf  26071  prlngsymquadlem  29244  ewlksfval  29985  isewlk  29986  ewlkinedg  29988  ispth  30109  trlsegvdeg  30625  frcond3  30667  numclwwlk3lem2  30782  chocin  31894  cmbr3  32007  pjoml3  32011  fh1  32017  xppreima2  33043  cosnopne  33086  swrdrndisj  33317  hauseqcn  34328  prsssdm  34347  ordtrestNEW  34351  ordtrest2NEW  34353  cndprobval  34864  ballotlemfrc  34958  bnj1421  35471  satffunlem  35906  satffunlem1lem2  35908  satffunlem2lem1  35909  satffunlem2lem2  35911  msrval  36043  msrf  36047  ismfs  36054  clsun  36872  poimirlem8  38312  itg2addnclem2  38356  heiborlem4  38498  heiborlem6  38500  heiborlem10  38504  shiftstableeq2  39165  pmodl42N  40658  polfvalN  40711  poldmj1N  40735  pmapj2N  40736  pnonsingN  40740  psubclinN  40755  poml4N  40760  osumcllem9N  40771  trnfsetN  40962  diainN  41864  djaffvalN  41940  djafvalN  41941  djajN  41944  dihmeetcl  42152  dihmeet2  42153  dochnoncon  42198  djhffval  42203  djhfval  42204  djhlj  42208  dochdmm1  42217  lclkrlem2g  42320  lclkrlem2v  42335  lcfrlem21  42370  lcfrlem24  42373  mapdunirnN  42457  baerlem5amN  42523  baerlem5bmN  42524  baerlem5abmN  42525  mapdheq4lem  42538  mapdh6lem1N  42540  mapdh6lem2N  42541  hdmap1l6lem1  42614  hdmap1l6lem2  42615  aomclem8  43821  disjrnmpt2  45939  dvsinax  46660  dvcosax  46673  nnfoctbdjlem  47202  smfpimcc  47555  smfsuplem2  47559  upgrimpths  48707  iscnrm3l  49762  invfn  49841  invpropdlem  49849  infsubc2d  49873  zeroopropdlem  50053  zeroopropd  50056