Theorem ineq12d 3848

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

Syntax hints:   → wi 4   = wceq 1523   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614

This theorem is referenced by:  csbin  4043  predeq123  5719  funprgOLD  5979  funtpgOLD  5981  funcnvtp  5989  offval  6946  ofrfval  6947  oev2  7648  isf32lem7  9219  ressval  15974  invffval  16465  invfval  16466  dfiso2  16479  isofn  16482  oppcinv  16487  zerooval  16696  isps  17249  dmdprd  18443  dprddisj  18454  dprdf1o  18477  dmdprdsplit2lem  18490  dmdprdpr  18494  pgpfaclem1  18526  isunit  18703  dfrhm2  18765  isrhm  18769  2idlval  19281  aspval  19376  ressmplbas2  19503  pjfval  20098  isconn  21264  connsuba  21271  ptbasin  21428  ptclsg  21466  qtopval  21546  rnelfmlem  21803  trust  22080  isnmhm  22597  uniioombllem2a  23396  dyaddisjlem  23409  dyaddisj  23410  i1faddlem  23505  i1fmullem  23506  limcflf  23690  ewlksfval  26553  isewlk  26554  ewlkinedg  26556  ispth  26675  trlsegvdeg  27205  frcond3  27249  numclwwlk3lem  27371  chocin  28482  cmbr3  28595  pjoml3  28599  fh1  28605  fnunres1  29543  xppreima2  29578  hauseqcn  30069  prsssdm  30091  ordtrestNEW  30095  ordtrest2NEW  30097  cndprobval  30623  ballotlemfrc  30716  bnj1421  31236  msrval  31561  msrf  31565  ismfs  31572  clsun  32448  poimirlem8  33547  itg2addnclem2  33592  heiborlem4  33743  heiborlem6  33745  heiborlem10  33749  pmodl42N  35455  polfvalN  35508  poldmj1N  35532  pmapj2N  35533  pnonsingN  35537  psubclinN  35552  poml4N  35557  osumcllem9N  35568  trnfsetN  35760  diainN  36663  djaffvalN  36739  djafvalN  36740  djajN  36743  dihmeetcl  36951  dihmeet2  36952  dochnoncon  36997  djhffval  37002  djhfval  37003  djhlj  37007  dochdmm1  37016  lclkrlem2g  37119  lclkrlem2v  37134  lcfrlem21  37169  lcfrlem24  37172  mapdunirnN  37256  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdheq4lem  37337  mapdh6lem1N  37339  mapdh6lem2N  37340  hdmap1l6lem1  37414  hdmap1l6lem2  37415  aomclem8  37948  csbingOLD  39369  disjrnmpt2  39689  dvsinax  40445  dvcosax  40459  nnfoctbdjlem  40990  smfpimcc  41335  smfsuplem2  41339  rhmval  42244