Theorem ineq1d 3813

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 3807	. 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 1483   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  diftpsn3OLD  4333  iinrab2  4583  disji2  4636  disjprg  4648  disjxun  4651  riinint  5382  fnresdisj  6001  fnimadisj  6012  fninfp  6440  ecinxp  7822  fiint  8237  fival  8318  marypha1lem  8339  kmlem12  8983  fin23lem12  9153  fin23lem30  9164  fin23lem33  9167  ttukeylem1  9331  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2  9465  fzval2  12329  fvinim0ffz  12587  limsupval  14205  limsupgval  14207  ello1  14246  elo1  14257  fsum1p  14482  incexclem  14568  fprod1p  14698  smuval2  15204  smueqlem  15212  smumul  15215  setsdm  15892  isacs2  16314  acsfiel  16315  isacs1i  16318  catcval  16746  resscatc  16755  acsficl  17171  lsmdisj3  18096  lsmdisj3a  18102  dprdres  18427  dprdz  18429  dpjdisj  18452  lspdisj2  19127  indistopon  20805  restopnb  20979  ordtrest2  21008  isnrm  21139  cmpcov  21192  cmpsublem  21202  cmpsub  21203  tgcmp  21204  uncmp  21206  hauscmplem  21209  nconnsubb  21226  isnlly  21272  dissnlocfin  21332  kgeni  21340  kgencn3  21361  ptcld  21416  ptcnplem  21424  alexsublem  21848  alexsubb  21850  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  tmdgsum2  21900  tsmsval2  21933  ustexsym  22019  metrest  22329  qtopbaslem  22562  cnheibor  22754  bndth  22757  lebnumii  22765  iscph  22970  csscld  23048  clsocv  23049  ovolicc2  23290  voliunlem3  23320  ioombl  23333  uniioombllem2  23351  uniioombllem4  23354  uniioombllem6  23356  mbflimsup  23433  taylfval  24113  chtval  24836  ppival  24853  ppival2  24854  ppival2g  24855  chtfl  24875  ppiprm  24877  chtprm  24879  chtnprm  24880  chtdif  24884  ppidif  24889  prmorcht  24904  chdmj2  28389  cmcmlem  28450  pjoml2  28470  fh2  28478  mdbr  29153  mdi  29154  mdbr3  29156  mdbr4  29157  dmdmd  29159  dmdbr3  29164  dmdbr4  29165  dmdi4  29166  dmdbr5  29167  mddmd2  29168  mdsl1i  29180  cvmdi  29183  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd1lem3  29186  mdslmd1lem4  29187  mdslmd1i  29188  mdslmd3i  29191  csmdsymi  29193  mdexchi  29194  atomli  29241  atabsi  29260  sumdmdlem2  29278  dmdbr5ati  29281  difuncomp  29369  disji2f  29390  disjif2  29394  disjxpin  29401  disjunsn  29407  fnresin  29430  locfinreflem  29907  iscref  29911  ordtrest2NEW  29969  ordtconnlem1  29970  carsgclctunlem1  30379  totprobd  30488  probmeasb  30492  ballotlemfval  30551  ballotlemfp1  30553  ballotlemgun  30586  chtvalz  30707  bnj1385  30903  bnj1326  31094  iccllysconn  31232  mvrsval  31402  mrsubvrs  31419  mpstval  31432  msubvrs  31457  nosupbnd2lem1  31861  neibastop2lem  32355  neibastop2  32356  neibastop3  32357  limsucncmpi  32444  bj-ismoore  33059  ptrest  33408  mblfinlem2  33447  sstotbnd2  33573  cntotbnd  33595  heibor  33620  l1cvat  34342  pmodlem2  35133  pmod2iN  35135  hlmod1i  35142  osumcllem3N  35244  osumcllem9N  35250  pexmidlem6N  35261  pl42lem1N  35265  istrnN  35444  djavalN  36424  dihmeetlem9N  36604  dihmeetlem11N  36606  dihmeetlem12N  36607  dihoml4  36666  djhval  36687  dochexmidlem6  36754  lclkrlem2b  36797  lcfrlem20  36851  lcfrlem23  36854  elrfi  37257  isnacs  37267  mrefg2  37270  mapfzcons2  37282  coeq0i  37316  eldioph2lem2  37324  aomclem8  37631  kelac1  37633  islmodfg  37639  lnr2i  37686  fgraphopab  37788  ntrkbimka  38336  ntrk0kbimka  38337  isotone2  38347  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  neicvgbex  38410  disjrnmpt2  39375  disjinfi  39380  uzinico2  39789  uzinico3  39790  fsumiunss  39807  lptre2pt  39872  limsupresre  39928  limsuplesup  39931  limsupresico  39932  limsupvaluz  39940  limsuplt2  39985  liminfval  39991  limsupge  39993  liminfgval  39994  liminfval2  40000  liminfresico  40003  liminflelimsuplem  40007  liminflelimsup  40008  stoweidlem50  40267  stoweidlem57  40274  subsaliuncllem  40575  sge0val  40583  sge0iunmptlemre  40632  nnfoctbdjlem  40672  iundjiun  40677  vonvolmbllem  40874  smfpimcclem  41013  smfsuplem1  41017  elbigo  42345  aacllem  42547