Theorem ineq12d 4118

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091

This theorem is used by:  csbin  4399  predeq123  6305  funcnvtp  6604  fnunres1  6652  ofrfvalg  7702  offval  7703  oev2  8535  isf32lem7  10441  ressval  17417  invffval  17939  invfval  17940  dfiso2  17953  isofn  17956  oppcinv  17961  zerooval  18176  cat1  18278  isps  18748  dmdprd  20220  dprddisj  20231  dprdf1o  20254  dmdprdsplit2lem  20267  dmdprdpr  20271  pgpfaclem1  20303  isunit  20609  dfrhm2  20710  isrhm  20715  rhmval  20744  2idlval  21550  pjfval  22018  aspval  22186  ressmplbas2  22341  isconn  23737  connsuba  23744  ptbasin  23902  ptclsg  23940  qtopval  24020  rnelfmlem  24277  trust  24554  isnmhm  25071  uniioombllem2a  25909  dyaddisjlem  25922  dyaddisj  25923  i1faddlem  26020  i1fmullem  26021  limcflf  26207  angmgmaddov1  29394  angmgmval  29400  prlngsymquadlem  29447  ewlksfval  30188  isewlk  30189  ewlkinedg  30191  ispth  30312  trlsegvdeg  30834  frcond3  30876  numclwwlk3lem2  30991  chocin  32103  cmbr3  32216  pjoml3  32220  fh1  32226  xppreima2  33293  cosnopne  33335  swrdrndisj  33565  hauseqcn  34577  prsssdm  34596  ordtrestNEW  34600  ordtrest2NEW  34602  cndprobval  35112  ballotlemfrc  35206  bnj1421  35719  satffunlem  36253  satffunlem1lem2  36255  satffunlem2lem1  36256  satffunlem2lem2  36258  msrval  36390  msrf  36394  ismfs  36401  clsun  37209  poimirlem8  38640  itg2addnclem2  38684  heiborlem4  38842  heiborlem6  38844  heiborlem10  38848  shiftstableeq2  39509  pmodl42N  41002  polfvalN  41055  poldmj1N  41079  pmapj2N  41080  pnonsingN  41084  psubclinN  41099  poml4N  41104  osumcllem9N  41115  trnfsetN  41306  diainN  42208  djaffvalN  42284  djafvalN  42285  djajN  42288  dihmeetcl  42496  dihmeet2  42497  dochnoncon  42542  djhffval  42547  djhfval  42548  djhlj  42552  dochdmm1  42561  lclkrlem2g  42664  lclkrlem2v  42679  lcfrlem21  42714  lcfrlem24  42717  mapdunirnN  42801  baerlem5amN  42867  baerlem5bmN  42868  baerlem5abmN  42869  mapdheq4lem  42882  mapdh6lem1N  42884  mapdh6lem2N  42885  hdmap1l6lem1  42958  hdmap1l6lem2  42959  aomclem8  44157  disjrnmpt2  46297  dvsinax  47017  dvcosax  47030  nnfoctbdjlem  47559  smfpimcc  47912  smfsuplem2  47916  upgrimpths  49101  iscnrm3l  50159  invfn  50238  invpropdlem  50246  infsubc2d  50270  zeroopropdlem  50458  zeroopropd  50461  parcoval  50856