Theorem ineq12d 4196

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933

This theorem is referenced by:  csbin  4417  predeq123  6291  funcnvtp  6599  fnunres1  6650  ofrfvalg  7679  offval  7680  oev2  8535  isf32lem7  10373  ressval  17254  invffval  17771  invfval  17772  dfiso2  17785  isofn  17788  oppcinv  17793  zerooval  18008  cat1  18110  isps  18578  dmdprd  19981  dprddisj  19992  dprdf1o  20015  dmdprdsplit2lem  20028  dmdprdpr  20032  pgpfaclem1  20064  isunit  20333  dfrhm2  20434  isrhm  20438  rhmval  20460  2idlval  21212  pjfval  21666  aspval  21833  ressmplbas2  21985  isconn  23351  connsuba  23358  ptbasin  23515  ptclsg  23553  qtopval  23633  rnelfmlem  23890  trust  24168  isnmhm  24685  uniioombllem2a  25535  dyaddisjlem  25548  dyaddisj  25549  i1faddlem  25646  i1fmullem  25647  limcflf  25834  ewlksfval  29581  isewlk  29582  ewlkinedg  29584  ispth  29703  trlsegvdeg  30208  frcond3  30250  numclwwlk3lem2  30365  chocin  31476  cmbr3  31589  pjoml3  31593  fh1  31599  xppreima2  32629  cosnopne  32671  swrdrndisj  32933  hauseqcn  33929  prsssdm  33948  ordtrestNEW  33952  ordtrest2NEW  33954  cndprobval  34465  ballotlemfrc  34559  bnj1421  35073  satffunlem  35423  satffunlem1lem2  35425  satffunlem2lem1  35426  satffunlem2lem2  35428  msrval  35560  msrf  35564  ismfs  35571  clsun  36346  poimirlem8  37652  itg2addnclem2  37696  heiborlem4  37838  heiborlem6  37840  heiborlem10  37844  pmodl42N  39870  polfvalN  39923  poldmj1N  39947  pmapj2N  39948  pnonsingN  39952  psubclinN  39967  poml4N  39972  osumcllem9N  39983  trnfsetN  40174  diainN  41076  djaffvalN  41152  djafvalN  41153  djajN  41156  dihmeetcl  41364  dihmeet2  41365  dochnoncon  41410  djhffval  41415  djhfval  41416  djhlj  41420  dochdmm1  41429  lclkrlem2g  41532  lclkrlem2v  41547  lcfrlem21  41582  lcfrlem24  41585  mapdunirnN  41669  baerlem5amN  41735  baerlem5bmN  41736  baerlem5abmN  41737  mapdheq4lem  41750  mapdh6lem1N  41752  mapdh6lem2N  41753  hdmap1l6lem1  41826  hdmap1l6lem2  41827  aomclem8  43085  disjrnmpt2  45212  dvsinax  45942  dvcosax  45955  nnfoctbdjlem  46484  smfpimcc  46837  smfsuplem2  46841  upgrimpths  47922  iscnrm3l  48925  invfn  49000  invpropdlem  49005  infsubc2d  49029  zeroopropdlem  49159  zeroopropd  49162