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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  csbin  4400  predeq123  6300  funcnvtp  6596  fnunres1  6644  ofrfvalg  7686  offval  7687  oev2  8510  isf32lem7  10361  ressval  17325  invffval  17847  invfval  17848  dfiso2  17861  isofn  17864  oppcinv  17869  zerooval  18084  cat1  18186  isps  18656  dmdprd  20127  dprddisj  20138  dprdf1o  20161  dmdprdsplit2lem  20174  dmdprdpr  20178  pgpfaclem1  20210  isunit  20514  dfrhm2  20615  isrhm  20620  rhmval  20649  2idlval  21453  pjfval  21919  aspval  22087  ressmplbas2  22242  isconn  23638  connsuba  23645  ptbasin  23803  ptclsg  23841  qtopval  23921  rnelfmlem  24178  trust  24455  isnmhm  24972  uniioombllem2a  25810  dyaddisjlem  25823  dyaddisj  25824  i1faddlem  25921  i1fmullem  25922  limcflf  26108  angmgmaddov1  29267  angmgmval  29273  prlngsymquadlem  29320  ewlksfval  30061  isewlk  30062  ewlkinedg  30064  ispth  30185  trlsegvdeg  30707  frcond3  30749  numclwwlk3lem2  30864  chocin  31976  cmbr3  32089  pjoml3  32093  fh1  32099  xppreima2  33124  cosnopne  33166  swrdrndisj  33397  hauseqcn  34408  prsssdm  34427  ordtrestNEW  34431  ordtrest2NEW  34433  cndprobval  34944  ballotlemfrc  35038  bnj1421  35551  satffunlem  35980  satffunlem1lem2  35982  satffunlem2lem1  35983  satffunlem2lem2  35985  msrval  36117  msrf  36121  ismfs  36128  clsun  36947  poimirlem8  38377  itg2addnclem2  38421  heiborlem4  38564  heiborlem6  38566  heiborlem10  38570  shiftstableeq2  39231  pmodl42N  40724  polfvalN  40777  poldmj1N  40801  pmapj2N  40802  pnonsingN  40806  psubclinN  40821  poml4N  40826  osumcllem9N  40837  trnfsetN  41028  diainN  41930  djaffvalN  42006  djafvalN  42007  djajN  42010  dihmeetcl  42218  dihmeet2  42219  dochnoncon  42264  djhffval  42269  djhfval  42270  djhlj  42274  dochdmm1  42283  lclkrlem2g  42386  lclkrlem2v  42401  lcfrlem21  42436  lcfrlem24  42439  mapdunirnN  42523  baerlem5amN  42589  baerlem5bmN  42590  baerlem5abmN  42591  mapdheq4lem  42604  mapdh6lem1N  42606  mapdh6lem2N  42607  hdmap1l6lem1  42680  hdmap1l6lem2  42681  aomclem8  43902  disjrnmpt2  46020  dvsinax  46741  dvcosax  46754  nnfoctbdjlem  47283  smfpimcc  47636  smfsuplem2  47640  upgrimpths  48825  iscnrm3l  49877  invfn  49956  invpropdlem  49964  infsubc2d  49988  zeroopropdlem  50168  zeroopropd  50171