Theorem ineq1d 3613

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 3607	. 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 1399   i^i cin 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396

This theorem is referenced by:  diftpsn3  4082  iinrab2  4306  disji2  4354  disjprg  4363  disjxun  4365  riinint  5172  fnresdisj  5599  fnimadisj  5609  fninfp  6000  ecinxp  7304  fiint  7712  fival  7787  marypha1lem  7808  kmlem12  8454  fin23lem12  8624  fin23lem30  8635  fin23lem33  8638  ttukeylem1  8802  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwe2  8932  fzval2  11596  injresinjlem  11824  limsupval  13299  limsupgval  13301  ello1  13340  elo1  13351  fsum1p  13570  incexclem  13650  fprod1p  13774  smuval2  14134  smueqlem  14142  smumul  14145  isacs2  15060  acsfiel  15061  isacs1i  15064  catcval  15492  resscatc  15501  acsficl  15918  lsmdisj3  16818  lsmdisj3a  16824  dprdres  17188  dprdz  17190  dpjdisj  17215  lspdisj2  17886  indistopon  19587  restopnb  19762  ordtrest2  19791  isnrm  19922  cmpcov  19975  cmpsublem  19985  cmpsub  19986  tgcmp  19987  uncmp  19989  hauscmplem  19992  nconsubb  20009  isnlly  20055  dissnlocfin  20115  kgeni  20123  kgencn3  20144  ptcld  20199  ptcnplem  20207  alexsublem  20629  alexsubb  20631  alexsubALTlem2  20633  alexsubALTlem4  20635  alexsubALT  20636  tmdgsum2  20680  tsmsval2  20713  ustexsym  20803  metrest  21112  qtopbaslem  21350  cnheibor  21540  bndth  21543  lebnumii  21551  iscph  21702  csscld  21774  clsocv  21775  ovolicc2  22018  voliunlem3  22047  ioombl  22060  uniioombllem2  22077  uniioombllem4  22080  uniioombllem6  22082  mbflimsup  22158  taylfval  22839  chtval  23501  ppival  23518  ppival2  23519  ppival2g  23520  chtfl  23540  ppiprm  23542  chtprm  23544  chtnprm  23545  chtdif  23549  ppidif  23554  prmorcht  23569  2pthlem2  24719  frgrancvvdeqlem4  25154  chdmj2  26565  cmcmlem  26626  pjoml2  26646  fh2  26654  mdbr  27329  mdi  27330  mdbr3  27332  mdbr4  27333  dmdmd  27335  dmdbr3  27340  dmdbr4  27341  dmdi4  27342  dmdbr5  27343  mddmd2  27344  mdsl1i  27356  cvmdi  27359  mdslmd1lem1  27360  mdslmd1lem2  27361  mdslmd1lem3  27362  mdslmd1lem4  27363  mdslmd1i  27364  mdslmd3i  27367  csmdsymi  27369  mdexchi  27370  atomli  27417  atabsi  27436  sumdmdlem2  27454  dmdbr5ati  27457  disji2f  27567  disjif2  27571  disjxpin  27577  disjunsn  27583  fnresin  27608  locfinreflem  27997  iscref  28001  ordtrest2NEW  28059  ordtconlem1  28060  carsgclctunlem1  28444  totprobd  28548  probmeasb  28552  ballotlemfval  28611  ballotlemfp1  28613  ballotlemgun  28646  iccllyscon  28884  mvrsval  29054  mrsubvrs  29071  mpstval  29084  msubvrs  29109  limsucncmpi  30063  ptrest  30213  mblfinlem2  30217  neibastop2lem  30344  neibastop2  30345  neibastop3  30346  sstotbnd2  30436  cntotbnd  30458  heibor  30483  elrfi  30792  isnacs  30802  mrefg2  30805  mapfzcons2  30817  coeq0i  30851  eldioph2lem2  30859  aomclem8  31173  kelac1  31175  islmodfg  31181  lnr2i  31233  fgraphopab  31338  lptre2pt  31812  stoweidlem50  31998  stoweidlem57  32005  elbigo  33372  aacllem  33550  bnj1385  34238  bnj1326  34429  l1cvat  35193  pmodlem2  35984  pmod2iN  35986  hlmod1i  35993  osumcllem3N  36095  osumcllem9N  36101  pexmidlem6N  36112  pl42lem1N  36116  istrnN  36295  djavalN  37275  dihmeetlem9N  37455  dihmeetlem11N  37457  dihmeetlem12N  37458  dihoml4  37517  djhval  37538  dochexmidlem6  37605  lclkrlem2b  37648  lcfrlem20  37702  lcfrlem23  37705