Theorem ineq12d 3958

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

Syntax hints:   → wi 4   = wceq 1632   ∩ cin 3714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722

This theorem is referenced by:  csbin  4153  predeq123  5842  funprgOLD  6102  funtpgOLD  6104  funcnvtp  6112  offval  7069  ofrfval  7070  oev2  7772  isf32lem7  9373  ressval  16129  invffval  16619  invfval  16620  dfiso2  16633  isofn  16636  oppcinv  16641  zerooval  16850  isps  17403  dmdprd  18597  dprddisj  18608  dprdf1o  18631  dmdprdsplit2lem  18644  dmdprdpr  18648  pgpfaclem1  18680  isunit  18857  dfrhm2  18919  isrhm  18923  2idlval  19435  aspval  19530  ressmplbas2  19657  pjfval  20252  isconn  21418  connsuba  21425  ptbasin  21582  ptclsg  21620  qtopval  21700  rnelfmlem  21957  trust  22234  isnmhm  22751  uniioombllem2a  23550  dyaddisjlem  23563  dyaddisj  23564  i1faddlem  23659  i1fmullem  23660  limcflf  23844  ewlksfval  26707  isewlk  26708  ewlkinedg  26710  ispth  26829  trlsegvdeg  27379  frcond3  27423  numclwwlk3lem  27552  chocin  28663  cmbr3  28776  pjoml3  28780  fh1  28786  fnunres1  29724  xppreima2  29759  hauseqcn  30250  prsssdm  30272  ordtrestNEW  30276  ordtrest2NEW  30278  cndprobval  30804  ballotlemfrc  30897  bnj1421  31417  msrval  31742  msrf  31746  ismfs  31753  clsun  32629  poimirlem8  33730  itg2addnclem2  33775  heiborlem4  33926  heiborlem6  33928  heiborlem10  33932  pmodl42N  35640  polfvalN  35693  poldmj1N  35717  pmapj2N  35718  pnonsingN  35722  psubclinN  35737  poml4N  35742  osumcllem9N  35753  trnfsetN  35945  diainN  36848  djaffvalN  36924  djafvalN  36925  djajN  36928  dihmeetcl  37136  dihmeet2  37137  dochnoncon  37182  djhffval  37187  djhfval  37188  djhlj  37192  dochdmm1  37201  lclkrlem2g  37304  lclkrlem2v  37319  lcfrlem21  37354  lcfrlem24  37357  mapdunirnN  37441  baerlem5amN  37507  baerlem5bmN  37508  baerlem5abmN  37509  mapdheq4lem  37522  mapdh6lem1N  37524  mapdh6lem2N  37525  hdmap1l6lem1  37599  hdmap1l6lem2  37600  aomclem8  38133  csbingOLD  39554  disjrnmpt2  39874  dvsinax  40630  dvcosax  40644  nnfoctbdjlem  41175  smfpimcc  41520  smfsuplem2  41524  rhmval  42429