Theorem ineq1d 3665

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 3659	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A i^i C ) = ( B i^i C ) )

Syntax hints:   -> wi 4   = wceq 1438   i^i cin 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3445

This theorem is referenced by:  diftpsn3  4137  iinrab2  4361  disji2  4409  disjprg  4418  disjxun  4420  riinint  5109  fnresdisj  5703  fnimadisj  5713  fninfp  6105  ecinxp  7448  fiint  7856  fival  7934  marypha1lem  7955  kmlem12  8597  fin23lem12  8767  fin23lem30  8778  fin23lem33  8781  ttukeylem1  8945  fpwwe2cbv  9061  fpwwe2lem2  9063  fpwwe2  9074  fzval2  11793  injresinjlem  12029  limsupval  13528  limsupvalOLD  13529  limsupgval  13531  ello1  13576  elo1  13587  fsum1p  13811  incexclem  13891  fprod1p  14019  smuval2  14453  smueqlem  14461  smumul  14464  isacs2  15556  acsfiel  15557  isacs1i  15560  catcval  15988  resscatc  15997  acsficl  16414  lsmdisj3  17330  lsmdisj3a  17336  dprdres  17658  dprdz  17660  dpjdisj  17683  lspdisj2  18347  indistopon  20012  restopnb  20187  ordtrest2  20216  isnrm  20347  cmpcov  20400  cmpsublem  20410  cmpsub  20411  tgcmp  20412  uncmp  20414  hauscmplem  20417  nconsubb  20434  isnlly  20480  dissnlocfin  20540  kgeni  20548  kgencn3  20569  ptcld  20624  ptcnplem  20632  alexsublem  21055  alexsubb  21057  alexsubALTlem2  21059  alexsubALTlem4  21061  alexsubALT  21062  tmdgsum2  21107  tsmsval2  21140  ustexsym  21226  metrest  21535  qtopbaslem  21775  cnheibor  21979  bndth  21982  lebnumii  21993  iscph  22144  csscld  22216  clsocv  22217  ovolicc2  22472  voliunlem3  22501  ioombl  22514  uniioombllem2  22536  uniioombllem2OLD  22537  uniioombllem4  22540  uniioombllem6  22542  mbflimsup  22619  mbflimsupOLD  22620  taylfval  23310  chtval  24033  ppival  24050  ppival2  24051  ppival2g  24052  chtfl  24072  ppiprm  24074  chtprm  24076  chtnprm  24077  chtdif  24081  ppidif  24086  prmorcht  24101  2pthlem2  25322  frgrancvvdeqlem4  25757  chdmj2  27179  cmcmlem  27240  pjoml2  27260  fh2  27268  mdbr  27943  mdi  27944  mdbr3  27946  mdbr4  27947  dmdmd  27949  dmdbr3  27954  dmdbr4  27955  dmdi4  27956  dmdbr5  27957  mddmd2  27958  mdsl1i  27970  cvmdi  27973  mdslmd1lem1  27974  mdslmd1lem2  27975  mdslmd1lem3  27976  mdslmd1lem4  27977  mdslmd1i  27978  mdslmd3i  27981  csmdsymi  27983  mdexchi  27984  atomli  28031  atabsi  28050  sumdmdlem2  28068  dmdbr5ati  28071  difuncomp  28166  disji2f  28187  disjif2  28191  disjxpin  28198  disjunsn  28204  fnresin  28228  locfinreflem  28673  iscref  28677  ordtrest2NEW  28735  ordtconlem1  28736  carsgclctunlem1  29155  totprobd  29265  probmeasb  29269  ballotlemfval  29328  ballotlemfp1  29330  ballotlemgun  29363  ballotlemgunOLD  29401  bnj1385  29650  bnj1326  29841  iccllyscon  29979  mvrsval  30149  mrsubvrs  30166  mpstval  30179  msubvrs  30204  neibastop2lem  31019  neibastop2  31020  neibastop3  31021  limsucncmpi  31108  ptrest  31901  mblfinlem2  31940  sstotbnd2  32068  cntotbnd  32090  heibor  32115  l1cvat  32588  pmodlem2  33379  pmod2iN  33381  hlmod1i  33388  osumcllem3N  33490  osumcllem9N  33496  pexmidlem6N  33507  pl42lem1N  33511  istrnN  33690  djavalN  34670  dihmeetlem9N  34850  dihmeetlem11N  34852  dihmeetlem12N  34853  dihoml4  34912  djhval  34933  dochexmidlem6  35000  lclkrlem2b  35043  lcfrlem20  35097  lcfrlem23  35100  elrfi  35503  isnacs  35513  mrefg2  35516  mapfzcons2  35528  coeq0i  35562  eldioph2lem2  35570  aomclem8  35887  kelac1  35889  islmodfg  35895  lnr2i  35943  fgraphopab  36055  disjrnmpt2  37361  disjinfi  37366  fsumiunss  37525  lptre2pt  37588  stoweidlem50  37779  stoweidlem57  37786  sge0val  38044  sge0iunmptlemre  38093  nnfoctbdjlem  38120  iundjiun  38125  elbigo  39756  aacllem  39934