Theorem ineq1d 3684

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 3678	. 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 1383   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468

This theorem is referenced by:  diftpsn3  4153  iinrab2  4378  disji2  4424  disjprg  4433  disjxun  4435  riinint  5249  fnresdisj  5681  fnimadisj  5691  fninfp  6083  ecinxp  7388  fiint  7799  fival  7874  marypha1lem  7895  kmlem12  8544  fin23lem12  8714  fin23lem30  8725  fin23lem33  8728  ttukeylem1  8892  fpwwe2cbv  9011  fpwwe2lem2  9013  fpwwe2  9024  fzval2  11686  injresinjlem  11907  limsupval  13279  limsupgval  13281  ello1  13320  elo1  13331  fsum1p  13550  incexclem  13630  fprod1p  13754  smuval2  14114  smueqlem  14122  smumul  14125  isacs2  15032  acsfiel  15033  isacs1i  15036  catcval  15402  resscatc  15411  acsficl  15780  lsmdisj3  16680  lsmdisj3a  16686  dprdres  17054  dprdz  17056  dpjdisj  17081  lspdisj2  17752  indistopon  19480  restopnb  19654  ordtrest2  19683  isnrm  19814  cmpcov  19867  cmpsublem  19877  cmpsub  19878  tgcmp  19879  uncmp  19881  hauscmplem  19884  bwthOLD  19889  nconsubb  19902  isnlly  19948  dissnlocfin  20008  kgeni  20016  kgencn3  20037  ptcld  20092  ptcnplem  20100  alexsublem  20522  alexsubb  20524  alexsubALTlem2  20526  alexsubALTlem4  20528  alexsubALT  20529  tmdgsum2  20573  tsmsval2  20606  ustexsym  20696  metrest  21005  qtopbaslem  21243  cnheibor  21433  bndth  21436  lebnumii  21444  iscph  21595  csscld  21667  clsocv  21668  ovolicc2  21911  voliunlem3  21940  ioombl  21953  uniioombllem2  21970  uniioombllem4  21973  uniioombllem6  21975  mbflimsup  22051  taylfval  22732  chtval  23362  ppival  23379  ppival2  23380  ppival2g  23381  chtfl  23401  ppiprm  23403  chtprm  23405  chtnprm  23406  chtdif  23410  ppidif  23415  prmorcht  23430  2pthlem2  24576  frgrancvvdeqlem4  25011  chdmj2  26426  cmcmlem  26487  pjoml2  26507  fh2  26515  mdbr  27191  mdi  27192  mdbr3  27194  mdbr4  27195  dmdmd  27197  dmdbr3  27202  dmdbr4  27203  dmdi4  27204  dmdbr5  27205  mddmd2  27206  mdsl1i  27218  cvmdi  27221  mdslmd1lem1  27222  mdslmd1lem2  27223  mdslmd1lem3  27224  mdslmd1lem4  27225  mdslmd1i  27226  mdslmd3i  27229  csmdsymi  27231  mdexchi  27232  atomli  27279  atabsi  27298  sumdmdlem2  27316  dmdbr5ati  27319  disji2f  27416  disjif2  27420  disjxpin  27425  disjunsn  27431  fnresin  27448  locfinreflem  27821  iscref  27825  ordtrest2NEW  27883  ordtconlem1  27884  totprobd  28343  probmeasb  28347  ballotlemfval  28406  ballotlemfp1  28408  ballotlemgun  28441  iccllyscon  28673  mvrsval  28843  mrsubvrs  28860  mpstval  28873  msubvrs  28898  limsucncmpi  29886  ptrest  30024  mblfinlem2  30028  neibastop2lem  30154  neibastop2  30155  neibastop3  30156  sstotbnd2  30246  cntotbnd  30268  heibor  30293  elrfi  30602  isnacs  30612  mrefg2  30615  mapfzcons2  30627  coeq0i  30662  eldioph2lem2  30670  aomclem8  30983  kelac1  30985  islmodfg  30991  lnr2i  31041  fgraphopab  31146  lptre2pt  31600  stoweidlem50  31786  stoweidlem57  31793  bnj1385  33759  bnj1326  33950  l1cvat  34655  pmodlem2  35446  pmod2iN  35448  hlmod1i  35455  osumcllem3N  35557  osumcllem9N  35563  pexmidlem6N  35574  pl42lem1N  35578  istrnN  35757  djavalN  36737  dihmeetlem9N  36917  dihmeetlem11N  36919  dihmeetlem12N  36920  dihoml4  36979  djhval  37000  dochexmidlem6  37067  lclkrlem2b  37110  lcfrlem20  37164  lcfrlem23  37167