Theorem ineq1d 3635

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 3629	. 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 1446   i^i cin 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413

This theorem is referenced by:  diftpsn3  4113  iinrab2  4344  disji2  4392  disjprg  4401  disjxun  4403  riinint  5094  fnresdisj  5691  fnimadisj  5701  fninfp  6096  ecinxp  7443  fiint  7853  fival  7931  marypha1lem  7952  kmlem12  8596  fin23lem12  8766  fin23lem30  8777  fin23lem33  8780  ttukeylem1  8944  fpwwe2cbv  9060  fpwwe2lem2  9062  fpwwe2  9073  fzval2  11794  injresinjlem  12031  limsupval  13543  limsupvalOLD  13544  limsupgval  13546  ello1  13591  elo1  13602  fsum1p  13826  incexclem  13906  fprod1p  14034  smuval2  14468  smueqlem  14476  smumul  14479  isacs2  15571  acsfiel  15572  isacs1i  15575  catcval  16003  resscatc  16012  acsficl  16429  lsmdisj3  17345  lsmdisj3a  17351  dprdres  17673  dprdz  17675  dpjdisj  17698  lspdisj2  18362  indistopon  20028  restopnb  20203  ordtrest2  20232  isnrm  20363  cmpcov  20416  cmpsublem  20426  cmpsub  20427  tgcmp  20428  uncmp  20430  hauscmplem  20433  nconsubb  20450  isnlly  20496  dissnlocfin  20556  kgeni  20564  kgencn3  20585  ptcld  20640  ptcnplem  20648  alexsublem  21071  alexsubb  21073  alexsubALTlem2  21075  alexsubALTlem4  21077  alexsubALT  21078  tmdgsum2  21123  tsmsval2  21156  ustexsym  21242  metrest  21551  qtopbaslem  21791  cnheibor  21995  bndth  21998  lebnumii  22009  iscph  22160  csscld  22232  clsocv  22233  ovolicc2  22488  voliunlem3  22517  ioombl  22530  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem4  22556  uniioombllem6  22558  mbflimsup  22635  mbflimsupOLD  22636  taylfval  23326  chtval  24049  ppival  24066  ppival2  24067  ppival2g  24068  chtfl  24088  ppiprm  24090  chtprm  24092  chtnprm  24093  chtdif  24097  ppidif  24102  prmorcht  24117  2pthlem2  25338  frgrancvvdeqlem4  25773  chdmj2  27195  cmcmlem  27256  pjoml2  27276  fh2  27284  mdbr  27959  mdi  27960  mdbr3  27962  mdbr4  27963  dmdmd  27965  dmdbr3  27970  dmdbr4  27971  dmdi4  27972  dmdbr5  27973  mddmd2  27974  mdsl1i  27986  cvmdi  27989  mdslmd1lem1  27990  mdslmd1lem2  27991  mdslmd1lem3  27992  mdslmd1lem4  27993  mdslmd1i  27994  mdslmd3i  27997  csmdsymi  27999  mdexchi  28000  atomli  28047  atabsi  28066  sumdmdlem2  28084  dmdbr5ati  28087  difuncomp  28178  disji2f  28199  disjif2  28203  disjxpin  28210  disjunsn  28216  fnresin  28240  locfinreflem  28679  iscref  28683  ordtrest2NEW  28741  ordtconlem1  28742  carsgclctunlem1  29161  totprobd  29271  probmeasb  29275  ballotlemfval  29334  ballotlemfp1  29336  ballotlemgun  29369  ballotlemgunOLD  29407  bnj1385  29656  bnj1326  29847  iccllyscon  29985  mvrsval  30155  mrsubvrs  30172  mpstval  30185  msubvrs  30210  neibastop2lem  31028  neibastop2  31029  neibastop3  31030  limsucncmpi  31117  ptrest  31951  mblfinlem2  31990  sstotbnd2  32118  cntotbnd  32140  heibor  32165  l1cvat  32633  pmodlem2  33424  pmod2iN  33426  hlmod1i  33433  osumcllem3N  33535  osumcllem9N  33541  pexmidlem6N  33552  pl42lem1N  33556  istrnN  33735  djavalN  34715  dihmeetlem9N  34895  dihmeetlem11N  34897  dihmeetlem12N  34898  dihoml4  34957  djhval  34978  dochexmidlem6  35045  lclkrlem2b  35088  lcfrlem20  35142  lcfrlem23  35145  elrfi  35548  isnacs  35558  mrefg2  35561  mapfzcons2  35573  coeq0i  35607  eldioph2lem2  35615  aomclem8  35931  kelac1  35933  islmodfg  35939  lnr2i  35987  fgraphopab  36099  disjrnmpt2  37473  disjinfi  37478  fsumiunss  37664  lptre2pt  37730  stoweidlem50  37921  stoweidlem57  37928  sge0val  38218  sge0iunmptlemre  38267  nnfoctbdjlem  38303  iundjiun  38308  elbigo  40466  aacllem  40644