Theorem ineq12d 3815

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

Syntax hints:   → wi 4   = wceq 1483   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  csbin  4010  predeq123  5681  funprgOLD  5941  funtpgOLD  5943  funcnvtp  5951  offval  6904  ofrfval  6905  oev2  7603  isf32lem7  9181  ressval  15927  invffval  16418  invfval  16419  dfiso2  16432  isofn  16435  oppcinv  16440  zerooval  16649  isps  17202  dmdprd  18397  dprddisj  18408  dprdf1o  18431  dmdprdsplit2lem  18444  dmdprdpr  18448  pgpfaclem1  18480  isunit  18657  dfrhm2  18717  isrhm  18721  2idlval  19233  aspval  19328  ressmplbas2  19455  pjfval  20050  isconn  21216  connsuba  21223  ptbasin  21380  ptclsg  21418  qtopval  21498  rnelfmlem  21756  trust  22033  isnmhm  22550  uniioombllem2a  23350  dyaddisjlem  23363  dyaddisj  23364  i1faddlem  23460  i1fmullem  23461  limcflf  23645  ewlksfval  26497  isewlk  26498  ewlkinedg  26500  ispth  26619  trlsegvdeg  27087  frcond3  27133  chocin  28354  cmbr3  28467  pjoml3  28471  fh1  28477  fnunres1  29417  xppreima2  29450  hauseqcn  29941  prsssdm  29963  ordtrestNEW  29967  ordtrest2NEW  29969  cndprobval  30495  ballotlemfrc  30588  bnj1421  31110  msrval  31435  msrf  31439  ismfs  31446  clsun  32323  poimirlem8  33417  itg2addnclem2  33462  heiborlem4  33613  heiborlem6  33615  heiborlem10  33619  pmodl42N  35137  polfvalN  35190  poldmj1N  35214  pmapj2N  35215  pnonsingN  35219  psubclinN  35234  poml4N  35239  osumcllem9N  35250  trnfsetN  35442  diainN  36346  djaffvalN  36422  djafvalN  36423  djajN  36426  dihmeetcl  36634  dihmeet2  36635  dochnoncon  36680  djhffval  36685  djhfval  36686  djhlj  36690  dochdmm1  36699  lclkrlem2g  36802  lclkrlem2v  36817  lcfrlem21  36852  lcfrlem24  36855  mapdunirnN  36939  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdheq4lem  37020  mapdh6lem1N  37022  mapdh6lem2N  37023  hdmap1l6lem1  37097  hdmap1l6lem2  37098  aomclem8  37631  csbingOLD  39054  disjrnmpt2  39375  dvsinax  40127  dvcosax  40141  nnfoctbdjlem  40672  smfpimcc  41014  smfsuplem2  41018  rhmval  41919