Theorem ineq12d 4151

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

Syntax hints:   → wi 4   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  csbin  4371  predeq123  6254  funcnvtp  6549  fnunres1  6598  ofrfvalg  7629  offval  7630  oev2  8449  isf32lem7  10273  ressval  17195  invffval  17717  invfval  17718  dfiso2  17731  isofn  17734  oppcinv  17739  zerooval  17954  cat1  18056  isps  18526  dmdprd  19967  dprddisj  19978  dprdf1o  20001  dmdprdsplit2lem  20014  dmdprdpr  20018  pgpfaclem1  20050  isunit  20345  dfrhm2  20446  isrhm  20450  rhmval  20472  2idlval  21245  pjfval  21682  aspval  21848  ressmplbas2  22003  isconn  23397  connsuba  23404  ptbasin  23561  ptclsg  23599  qtopval  23679  rnelfmlem  23936  trust  24213  isnmhm  24730  uniioombllem2a  25568  dyaddisjlem  25581  dyaddisj  25582  i1faddlem  25679  i1fmullem  25680  limcflf  25867  ewlksfval  29689  isewlk  29690  ewlkinedg  29692  ispth  29808  trlsegvdeg  30316  frcond3  30358  numclwwlk3lem2  30473  chocin  31585  cmbr3  31698  pjoml3  31702  fh1  31708  xppreima2  32744  cosnopne  32787  swrdrndisj  33037  hauseqcn  34091  prsssdm  34110  ordtrestNEW  34114  ordtrest2NEW  34116  cndprobval  34626  ballotlemfrc  34720  bnj1421  35233  satffunlem  35638  satffunlem1lem2  35640  satffunlem2lem1  35641  satffunlem2lem2  35643  msrval  35775  msrf  35779  ismfs  35786  clsun  36565  poimirlem8  38004  itg2addnclem2  38048  heiborlem4  38190  heiborlem6  38192  heiborlem10  38196  shiftstableeq2  38859  pmodl42N  40352  polfvalN  40405  poldmj1N  40429  pmapj2N  40430  pnonsingN  40434  psubclinN  40449  poml4N  40454  osumcllem9N  40465  trnfsetN  40656  diainN  41558  djaffvalN  41634  djafvalN  41635  djajN  41638  dihmeetcl  41846  dihmeet2  41847  dochnoncon  41892  djhffval  41897  djhfval  41898  djhlj  41902  dochdmm1  41911  lclkrlem2g  42014  lclkrlem2v  42029  lcfrlem21  42064  lcfrlem24  42067  mapdunirnN  42151  baerlem5amN  42217  baerlem5bmN  42218  baerlem5abmN  42219  mapdheq4lem  42232  mapdh6lem1N  42234  mapdh6lem2N  42235  hdmap1l6lem1  42308  hdmap1l6lem2  42309  aomclem8  43515  disjrnmpt2  45643  dvsinax  46364  dvcosax  46377  nnfoctbdjlem  46906  smfpimcc  47259  smfsuplem2  47263  upgrimpths  48408  iscnrm3l  49449  invfn  49528  invpropdlem  49536  infsubc2d  49560  zeroopropdlem  49740  zeroopropd  49743