Theorem ineq1d 3699

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 3693	. 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 1379   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  diftpsn3  4165  iinrab2  4388  disji2  4434  disjprg  4443  disjxun  4445  riinint  5259  fnresdisj  5691  fnimadisj  5701  fninfp  6088  ecinxp  7386  fiint  7797  fival  7872  marypha1lem  7893  kmlem12  8541  fin23lem12  8711  fin23lem30  8722  fin23lem33  8725  ttukeylem1  8889  fpwwe2cbv  9008  fpwwe2lem2  9010  fpwwe2  9021  fzval2  11675  injresinjlem  11893  limsupval  13260  limsupgval  13262  ello1  13301  elo1  13312  fsum1p  13531  incexclem  13611  smuval2  13991  smueqlem  13999  smumul  14002  isacs2  14908  acsfiel  14909  isacs1i  14912  catcval  15281  resscatc  15290  acsficl  15658  lsmdisj3  16507  lsmdisj3a  16513  dprdres  16877  dprdz  16879  dpjdisj  16904  lspdisj2  17573  indistopon  19296  restopnb  19470  ordtrest2  19499  isnrm  19630  cmpcov  19683  cmpsublem  19693  cmpsub  19694  tgcmp  19695  uncmp  19697  hauscmplem  19700  bwthOLD  19705  nconsubb  19718  isnlly  19764  kgeni  19801  kgencn3  19822  ptcld  19877  ptcnplem  19885  alexsublem  20307  alexsubb  20309  alexsubALTlem2  20311  alexsubALTlem4  20313  alexsubALT  20314  tmdgsum2  20358  tsmsval2  20391  ustexsym  20481  metrest  20790  qtopbaslem  21028  cnheibor  21218  bndth  21221  lebnumii  21229  iscph  21380  csscld  21452  clsocv  21453  ovolicc2  21696  voliunlem3  21725  ioombl  21738  uniioombllem2  21755  uniioombllem4  21758  uniioombllem6  21760  mbflimsup  21836  taylfval  22516  chtval  23140  ppival  23157  ppival2  23158  ppival2g  23159  chtfl  23179  ppiprm  23181  chtprm  23183  chtnprm  23184  chtdif  23188  ppidif  23193  prmorcht  23208  2pthlem2  24302  frgrancvvdeqlem4  24738  chdmj2  26152  cmcmlem  26213  pjoml2  26233  fh2  26241  mdbr  26917  mdi  26918  mdbr3  26920  mdbr4  26921  dmdmd  26923  dmdbr3  26928  dmdbr4  26929  dmdi4  26930  dmdbr5  26931  mddmd2  26932  mdsl1i  26944  cvmdi  26947  mdslmd1lem1  26948  mdslmd1lem2  26949  mdslmd1lem3  26950  mdslmd1lem4  26951  mdslmd1i  26952  mdslmd3i  26955  csmdsymi  26957  mdexchi  26958  atomli  27005  atabsi  27024  sumdmdlem2  27042  dmdbr5ati  27045  disji2f  27139  disjif2  27143  disjxpin  27148  disjunsn  27154  fnresin  27171  ordtrest2NEW  27569  ordtconlem1  27570  totprobd  28033  probmeasb  28037  ballotlemfval  28096  ballotlemfp1  28098  ballotlemgun  28131  iccllyscon  28363  fprod1p  28702  limsucncmpi  29515  ptrest  29653  mblfinlem2  29657  neibastop2lem  29809  neibastop2  29810  neibastop3  29811  sstotbnd2  29901  cntotbnd  29923  heibor  29948  elrfi  30258  isnacs  30268  mrefg2  30271  mapfzcons2  30283  coeq0i  30318  eldioph2lem2  30326  aomclem8  30639  kelac1  30641  islmodfg  30647  lnr2i  30697  fgraphopab  30803  lptre2pt  31210  stoweidlem50  31378  stoweidlem57  31385  bnj1385  32988  bnj1326  33179  l1cvat  33870  pmodlem2  34661  pmod2iN  34663  hlmod1i  34670  osumcllem3N  34772  osumcllem9N  34778  pexmidlem6N  34789  pl42lem1N  34793  istrnN  34971  djavalN  35950  dihmeetlem9N  36130  dihmeetlem11N  36132  dihmeetlem12N  36133  dihoml4  36192  djhval  36213  dochexmidlem6  36280  lclkrlem2b  36323  lcfrlem20  36377  lcfrlem23  36380