Theorem ineq1d 3572

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
ineq1d	|- ( ph -> ( A i^i C ) = ( B i^i C ) )

Proof of Theorem ineq1d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 |- ( ph -> A = B )
2		ineq1 3566	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
3	1, 2	syl 16	1 |- ( ph -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   = wceq 1369   i^i cin 3348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356

This theorem is referenced by:  diftpsn3  4033  iinrab2  4254  disji2  4300  disjprg  4309  disjxun  4311  riinint  5117  fnresdisj  5542  fnimadisj  5552  fninfp  5926  ecinxp  7196  fiint  7609  fival  7683  marypha1lem  7704  kmlem12  8351  fin23lem12  8521  fin23lem30  8532  fin23lem33  8535  ttukeylem1  8699  fpwwe2cbv  8818  fpwwe2lem2  8820  fpwwe2  8831  fzval2  11461  injresinjlem  11659  limsupval  12973  limsupgval  12975  ello1  13014  elo1  13025  fsum1p  13243  incexclem  13320  smuval2  13699  smueqlem  13707  smumul  13710  isacs2  14612  acsfiel  14613  isacs1i  14616  catcval  14985  resscatc  14994  acsficl  15362  lsmdisj3  16201  lsmdisj3a  16207  dprdres  16547  dprdz  16549  dpjdisj  16574  lspdisj2  17230  indistopon  18627  restopnb  18801  ordtrest2  18830  isnrm  18961  cmpcov  19014  cmpsublem  19024  cmpsub  19025  tgcmp  19026  uncmp  19028  hauscmplem  19031  bwthOLD  19036  nconsubb  19049  isnlly  19095  kgeni  19132  kgencn3  19153  ptcld  19208  ptcnplem  19216  alexsublem  19638  alexsubb  19640  alexsubALTlem2  19642  alexsubALTlem4  19644  alexsubALT  19645  tmdgsum2  19689  tsmsval2  19722  ustexsym  19812  metrest  20121  qtopbaslem  20359  cnheibor  20549  bndth  20552  lebnumii  20560  iscph  20711  csscld  20783  clsocv  20784  ovolicc2  21027  voliunlem3  21055  ioombl  21068  uniioombllem2  21085  uniioombllem4  21088  uniioombllem6  21090  mbflimsup  21166  taylfval  21846  chtval  22470  ppival  22487  ppival2  22488  ppival2g  22489  chtfl  22509  ppiprm  22511  chtprm  22513  chtnprm  22514  chtdif  22518  ppidif  22523  prmorcht  22538  2pthlem2  23517  chdmj2  24955  cmcmlem  25016  pjoml2  25036  fh2  25044  mdbr  25720  mdi  25721  mdbr3  25723  mdbr4  25724  dmdmd  25726  dmdbr3  25731  dmdbr4  25732  dmdi4  25733  dmdbr5  25734  mddmd2  25735  mdsl1i  25747  cvmdi  25750  mdslmd1lem1  25751  mdslmd1lem2  25752  mdslmd1lem3  25753  mdslmd1lem4  25754  mdslmd1i  25755  mdslmd3i  25758  csmdsymi  25760  mdexchi  25761  atomli  25808  atabsi  25827  sumdmdlem2  25845  dmdbr5ati  25848  disji2f  25943  disjif2  25947  disjxpin  25952  disjunsn  25958  fnresin  25969  ordtrest2NEW  26375  ordtconlem1  26376  totprobd  26831  probmeasb  26835  ballotlemfval  26894  ballotlemfp1  26896  ballotlemgun  26929  iccllyscon  27161  fprod1p  27500  limsucncmpi  28313  ptrest  28451  mblfinlem2  28455  neibastop2lem  28607  neibastop2  28608  neibastop3  28609  sstotbnd2  28699  cntotbnd  28721  heibor  28746  elrfi  29056  isnacs  29066  mrefg2  29069  mapfzcons2  29081  coeq0i  29117  eldioph2lem2  29125  aomclem8  29440  kelac1  29442  islmodfg  29448  lnr2i  29498  fgraphopab  29604  stoweidlem50  29871  stoweidlem57  29878  frgrancvvdeqlem4  30652  bnj1385  31922  bnj1326  32113  l1cvat  32796  pmodlem2  33587  pmod2iN  33589  hlmod1i  33596  osumcllem3N  33698  osumcllem9N  33704  pexmidlem6N  33715  pl42lem1N  33719  istrnN  33897  djavalN  34876  dihmeetlem9N  35056  dihmeetlem11N  35058  dihmeetlem12N  35059  dihoml4  35118  djhval  35139  dochexmidlem6  35206  lclkrlem2b  35249  lcfrlem20  35303  lcfrlem23  35306