Theorem ineq12d 3793

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

Syntax hints:   → wi 4   = wceq 1480   ∩ cin 3554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562

This theorem is referenced by:  csbin  3982  predeq123  5640  funprgOLD  5899  funtpgOLD  5901  funcnvtp  5909  offval  6857  ofrfval  6858  oev2  7548  isf32lem7  9125  ressval  15848  invffval  16339  invfval  16340  dfiso2  16353  isofn  16356  oppcinv  16361  zerooval  16570  isps  17123  dmdprd  18318  dprddisj  18329  dprdf1o  18352  dmdprdsplit2lem  18365  dmdprdpr  18369  pgpfaclem1  18401  isunit  18578  dfrhm2  18638  isrhm  18642  2idlval  19152  aspval  19247  ressmplbas2  19374  pjfval  19969  isconn  21126  connsuba  21133  ptbasin  21290  ptclsg  21328  qtopval  21408  rnelfmlem  21666  trust  21943  isnmhm  22460  uniioombllem2a  23256  dyaddisjlem  23269  dyaddisj  23270  i1faddlem  23366  i1fmullem  23367  limcflf  23551  ewlksfval  26367  isewlk  26368  ewlkinedg  26370  ispth  26488  trlsegvdeg  26953  frcond3  26998  chocin  28203  cmbr3  28316  pjoml3  28320  fh1  28326  xppreima2  29292  hauseqcn  29723  prsssdm  29745  ordtrestNEW  29749  ordtrest2NEW  29751  cndprobval  30276  ballotlemfrc  30369  bnj1421  30818  msrval  31143  msrf  31147  ismfs  31154  clsun  31965  poimirlem8  33049  itg2addnclem2  33094  heiborlem4  33245  heiborlem6  33247  heiborlem10  33251  pmodl42N  34617  polfvalN  34670  poldmj1N  34694  pmapj2N  34695  pnonsingN  34699  psubclinN  34714  poml4N  34719  osumcllem9N  34730  trnfsetN  34922  diainN  35826  djaffvalN  35902  djafvalN  35903  djajN  35906  dihmeetcl  36114  dihmeet2  36115  dochnoncon  36160  djhffval  36165  djhfval  36166  djhlj  36170  dochdmm1  36179  lclkrlem2g  36282  lclkrlem2v  36297  lcfrlem21  36332  lcfrlem24  36335  mapdunirnN  36419  baerlem5amN  36485  baerlem5bmN  36486  baerlem5abmN  36487  mapdheq4lem  36500  mapdh6lem1N  36502  mapdh6lem2N  36503  hdmap1l6lem1  36577  hdmap1l6lem2  36578  aomclem8  37111  csbingOLD  38537  disjrnmpt2  38849  dvsinax  39432  dvcosax  39447  nnfoctbdjlem  39979  smfpimcc  40321  smfsuplem2  40325  rhmval  41207