Theorem ineq1d 3539

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 3533	. 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 1362   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  diftpsn3  4000  iinrab2  4221  disji2  4267  disjprg  4276  disjxun  4278  riinint  5083  fnresdisj  5509  fnimadisj  5519  fninfp  5892  ecinxp  7163  fiint  7576  fival  7650  marypha1lem  7671  kmlem12  8318  fin23lem12  8488  fin23lem30  8499  fin23lem33  8502  ttukeylem1  8666  fpwwe2cbv  8784  fpwwe2lem2  8786  fpwwe2  8797  fzval2  11426  injresinjlem  11621  limsupval  12935  limsupgval  12937  ello1  12976  elo1  12987  fsum1p  13205  incexclem  13281  smuval2  13660  smueqlem  13668  smumul  13671  isacs2  14573  acsfiel  14574  isacs1i  14577  catcval  14946  resscatc  14955  acsficl  15323  lsmdisj3  16159  lsmdisj3a  16165  dprdres  16498  dprdz  16500  dpjdisj  16525  lspdisj2  17129  indistopon  18446  restopnb  18620  ordtrest2  18649  isnrm  18780  cmpcov  18833  cmpsublem  18843  cmpsub  18844  tgcmp  18845  uncmp  18847  hauscmplem  18850  bwthOLD  18855  nconsubb  18868  isnlly  18914  kgeni  18951  kgencn3  18972  ptcld  19027  ptcnplem  19035  alexsublem  19457  alexsubb  19459  alexsubALTlem2  19461  alexsubALTlem4  19463  alexsubALT  19464  tmdgsum2  19508  tsmsval2  19541  ustexsym  19631  metrest  19940  qtopbaslem  20178  cnheibor  20368  bndth  20371  lebnumii  20379  iscph  20530  csscld  20602  clsocv  20603  ovolicc2  20846  voliunlem3  20874  ioombl  20887  uniioombllem2  20904  uniioombllem4  20907  uniioombllem6  20909  mbflimsup  20985  taylfval  21708  chtval  22332  ppival  22349  ppival2  22350  ppival2g  22351  chtfl  22371  ppiprm  22373  chtprm  22375  chtnprm  22376  chtdif  22380  ppidif  22385  prmorcht  22400  2pthlem2  23317  chdmj2  24755  cmcmlem  24816  pjoml2  24836  fh2  24844  mdbr  25520  mdi  25521  mdbr3  25523  mdbr4  25524  dmdmd  25526  dmdbr3  25531  dmdbr4  25532  dmdi4  25533  dmdbr5  25534  mddmd2  25535  mdsl1i  25547  cvmdi  25550  mdslmd1lem1  25551  mdslmd1lem2  25552  mdslmd1lem3  25553  mdslmd1lem4  25554  mdslmd1i  25555  mdslmd3i  25558  csmdsymi  25560  mdexchi  25561  atomli  25608  atabsi  25627  sumdmdlem2  25645  dmdbr5ati  25648  disji2f  25744  disjif2  25748  disjxpin  25753  disjunsn  25759  fnresin  25770  ordtrest2NEW  26206  ordtconlem1  26207  totprobd  26656  probmeasb  26660  ballotlemfval  26719  ballotlemfp1  26721  ballotlemgun  26754  iccllyscon  26986  fprod1p  27324  limsucncmpi  28138  ptrest  28266  mblfinlem2  28270  neibastop2lem  28422  neibastop2  28423  neibastop3  28424  sstotbnd2  28514  cntotbnd  28536  heibor  28561  elrfi  28872  isnacs  28882  mrefg2  28885  mapfzcons2  28897  coeq0i  28933  eldioph2lem2  28941  aomclem8  29256  kelac1  29258  islmodfg  29264  lnr2i  29314  fgraphopab  29420  stoweidlem50  29688  stoweidlem57  29695  frgrancvvdeqlem4  30469  bnj1385  31525  bnj1326  31716  l1cvat  32270  pmodlem2  33061  pmod2iN  33063  hlmod1i  33070  osumcllem3N  33172  osumcllem9N  33178  pexmidlem6N  33189  pl42lem1N  33193  istrnN  33371  djavalN  34350  dihmeetlem9N  34530  dihmeetlem11N  34532  dihmeetlem12N  34533  dihoml4  34592  djhval  34613  dochexmidlem6  34680  lclkrlem2b  34723  lcfrlem20  34777  lcfrlem23  34780