Theorem ineq1d 3501

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 3495	. 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 1649   i^i cin 3279

This theorem is referenced by:  diftpsn3  3897  iinrab2  4114  disji2  4159  disjprg  4168  disjxun  4170  riinint  5085  fnresdisj  5514  fnimadisj  5524  ecinxp  6938  fiint  7342  fival  7375  marypha1lem  7396  kmlem12  7997  fin23lem12  8167  fin23lem30  8178  fin23lem33  8181  ttukeylem1  8345  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwe2  8474  fzval2  11002  injresinjlem  11154  limsupval  12223  limsupgval  12225  ello1  12264  elo1  12275  fsum1p  12494  incexclem  12571  smuval2  12949  smueqlem  12957  smumul  12960  isacs2  13833  acsfiel  13834  isacs1i  13837  catcval  14206  resscatc  14215  acsficl  14552  lsmdisj3  15270  lsmdisj3a  15276  dprdres  15541  dprdz  15543  dpjdisj  15566  lspdisj2  16154  indistopon  17020  restopnb  17193  ordtrest2  17222  isnrm  17353  cmpcov  17406  cmpsublem  17416  cmpsub  17417  tgcmp  17418  uncmp  17420  hauscmplem  17423  nconsubb  17439  isnlly  17485  kgeni  17522  kgencn3  17543  ptcld  17598  ptcnplem  17606  alexsublem  18028  alexsubb  18030  alexsubALTlem2  18032  alexsubALTlem4  18034  alexsubALT  18035  tmdgsum2  18079  tsmsval2  18112  ustexsym  18198  metrest  18507  qtopbaslem  18745  cnheibor  18933  bndth  18936  lebnumii  18944  iscph  19086  csscld  19156  clsocv  19157  ovolicc2  19371  voliunlem3  19399  ioombl  19412  uniioombllem2  19428  uniioombllem4  19431  uniioombllem6  19433  mbflimsup  19511  taylfval  20228  chtval  20846  ppival  20863  ppival2  20864  ppival2g  20865  chtfl  20885  ppiprm  20887  chtprm  20889  chtnprm  20890  chtdif  20894  ppidif  20899  prmorcht  20914  2pthlem2  21549  chdmj2  22985  cmcmlem  23046  pjoml2  23066  fh2  23074  mdbr  23750  mdi  23751  mdbr3  23753  mdbr4  23754  dmdmd  23756  dmdbr3  23761  dmdbr4  23762  dmdi4  23763  dmdbr5  23764  mddmd2  23765  mdsl1i  23777  cvmdi  23780  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd1lem3  23783  mdslmd1lem4  23784  mdslmd1i  23785  mdslmd3i  23788  csmdsymi  23790  mdexchi  23791  atomli  23838  atabsi  23857  sumdmdlem2  23875  dmdbr5ati  23878  disji2f  23972  disjif2  23976  disjxpin  23981  totprobd  24637  probmeasb  24641  ballotlemfval  24700  ballotlemfp1  24702  ballotlemgun  24735  iccllyscon  24890  fprod1p  25244  limsucncmpi  26099  mblfinlem  26143  neibastop2lem  26279  neibastop2  26280  neibastop3  26281  sstotbnd2  26373  cntotbnd  26395  heibor  26420  fninfp  26625  elrfi  26638  isnacs  26648  mrefg2  26651  mapfzcons2  26665  coeq0i  26701  eldioph2lem2  26709  aomclem8  27027  kelac1  27029  islmodfg  27035  lnr2i  27188  fgraphopab  27397  stoweidlem50  27666  stoweidlem57  27673  frgrancvvdeqlem4  28136  bnj1385  28910  bnj1326  29101  l1cvat  29538  pmodlem2  30329  pmod2iN  30331  hlmod1i  30338  osumcllem3N  30440  osumcllem9N  30446  pexmidlem6N  30457  pl42lem1N  30461  istrnN  30639  djavalN  31618  dihmeetlem9N  31798  dihmeetlem11N  31800  dihmeetlem12N  31801  dihoml4  31860  djhval  31881  dochexmidlem6  31948  lclkrlem2b  31991  lcfrlem20  32045  lcfrlem23  32048

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287