Theorem ineq12d 4190

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

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3935

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943

This theorem is referenced by:  csbin  4391  predeq123  6149  funcnvtp  6417  offval  7416  ofrfval  7417  oev2  8148  isf32lem7  9781  ressval  16551  invffval  17028  invfval  17029  dfiso2  17042  isofn  17045  oppcinv  17050  zerooval  17259  isps  17812  dmdprd  19120  dprddisj  19131  dprdf1o  19154  dmdprdsplit2lem  19167  dmdprdpr  19171  pgpfaclem1  19203  isunit  19407  dfrhm2  19469  isrhm  19473  2idlval  20006  aspval  20102  ressmplbas2  20236  pjfval  20850  isconn  22021  connsuba  22028  ptbasin  22185  ptclsg  22223  qtopval  22303  rnelfmlem  22560  trust  22838  isnmhm  23355  uniioombllem2a  24183  dyaddisjlem  24196  dyaddisj  24197  i1faddlem  24294  i1fmullem  24295  limcflf  24479  ewlksfval  27383  isewlk  27384  ewlkinedg  27386  ispth  27504  trlsegvdeg  28006  frcond3  28048  numclwwlk3lem2  28163  chocin  29272  cmbr3  29385  pjoml3  29389  fh1  29395  fnunres1  30356  xppreima2  30395  cosnopne  30430  swrdrndisj  30631  hauseqcn  31138  prsssdm  31160  ordtrestNEW  31164  ordtrest2NEW  31166  cndprobval  31691  ballotlemfrc  31784  bnj1421  32314  satffunlem  32648  satffunlem1lem2  32650  satffunlem2lem1  32651  satffunlem2lem2  32653  msrval  32785  msrf  32789  ismfs  32796  clsun  33676  poimirlem8  34915  itg2addnclem2  34959  heiborlem4  35107  heiborlem6  35109  heiborlem10  35113  pmodl42N  37002  polfvalN  37055  poldmj1N  37079  pmapj2N  37080  pnonsingN  37084  psubclinN  37099  poml4N  37104  osumcllem9N  37115  trnfsetN  37306  diainN  38208  djaffvalN  38284  djafvalN  38285  djajN  38288  dihmeetcl  38496  dihmeet2  38497  dochnoncon  38542  djhffval  38547  djhfval  38548  djhlj  38552  dochdmm1  38561  lclkrlem2g  38664  lclkrlem2v  38679  lcfrlem21  38714  lcfrlem24  38717  mapdunirnN  38801  baerlem5amN  38867  baerlem5bmN  38868  baerlem5abmN  38869  mapdheq4lem  38882  mapdh6lem1N  38884  mapdh6lem2N  38885  hdmap1l6lem1  38958  hdmap1l6lem2  38959  aomclem8  39710  disjrnmpt2  41498  dvsinax  42246  dvcosax  42260  nnfoctbdjlem  42786  smfpimcc  43131  smfsuplem2  43135  rhmval  44239