Theorem ineq12d 4116

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

Syntax hints:   → wi 4   = wceq 1525   ∩ cin 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-in 3872

This theorem is referenced by:  csbin  4312  predeq123  6031  funcnvtp  6294  offval  7281  ofrfval  7282  oev2  8006  isf32lem7  9634  ressval  16384  invffval  16861  invfval  16862  dfiso2  16875  isofn  16878  oppcinv  16883  zerooval  17092  isps  17645  dmdprd  18841  dprddisj  18852  dprdf1o  18875  dmdprdsplit2lem  18888  dmdprdpr  18892  pgpfaclem1  18924  isunit  19101  dfrhm2  19163  isrhm  19167  2idlval  19699  aspval  19794  ressmplbas2  19927  pjfval  20536  isconn  21709  connsuba  21716  ptbasin  21873  ptclsg  21911  qtopval  21991  rnelfmlem  22248  trust  22525  isnmhm  23042  uniioombllem2a  23870  dyaddisjlem  23883  dyaddisj  23884  i1faddlem  23981  i1fmullem  23982  limcflf  24166  ewlksfval  27070  isewlk  27071  ewlkinedg  27073  ispth  27190  trlsegvdeg  27692  frcond3  27736  numclwwlk3lem2  27851  chocin  28959  cmbr3  29072  pjoml3  29076  fh1  29082  fnunres1  30042  xppreima2  30081  cosnopne  30114  hauseqcn  30751  prsssdm  30773  ordtrestNEW  30777  ordtrest2NEW  30779  cndprobval  31304  ballotlemfrc  31397  bnj1421  31924  satffunlem  32258  satffunlem1lem2  32260  satffunlem2lem1  32261  satffunlem2lem2  32263  msrval  32395  msrf  32399  ismfs  32406  clsun  33287  poimirlem8  34452  itg2addnclem2  34496  heiborlem4  34645  heiborlem6  34647  heiborlem10  34651  pmodl42N  36539  polfvalN  36592  poldmj1N  36616  pmapj2N  36617  pnonsingN  36621  psubclinN  36636  poml4N  36641  osumcllem9N  36652  trnfsetN  36843  diainN  37745  djaffvalN  37821  djafvalN  37822  djajN  37825  dihmeetcl  38033  dihmeet2  38034  dochnoncon  38079  djhffval  38084  djhfval  38085  djhlj  38089  dochdmm1  38098  lclkrlem2g  38201  lclkrlem2v  38216  lcfrlem21  38251  lcfrlem24  38254  mapdunirnN  38338  baerlem5amN  38404  baerlem5bmN  38405  baerlem5abmN  38406  mapdheq4lem  38419  mapdh6lem1N  38421  mapdh6lem2N  38422  hdmap1l6lem1  38495  hdmap1l6lem2  38496  aomclem8  39167  disjrnmpt2  41010  dvsinax  41760  dvcosax  41774  nnfoctbdjlem  42301  smfpimcc  42646  smfsuplem2  42650  rhmval  43690