Theorem oveqd 7447

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 7436	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  oveq123d  7451  oveqdr  7458  csbov  7475  csbov12g  7476  ovmpodxf  7582  oprssov  7601  2mpo0  7681  ofeqd  7698  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabovd  8105  mptmpoopabbrdOLDOLD  8106  mptmpoopabovdOLD  8107  el2mpocsbcl  8108  fnmpoovd  8110  frecseq123  8305  ruclem1  16263  vdwapval  17006  vdwapid1  17008  vdwmc2  17012  vdwpc  17013  vdwlem5  17018  vdwlem8  17021  vdwlem13  17026  prdsval  17501  prdsdsval2  17530  pwsplusgval  17536  pwsmulrval  17537  pwsvscafval  17540  imasval  17557  iscat  17716  iscatd  17717  catidex  17718  catideu  17719  cidfval  17720  cidval  17721  catidd  17724  iscatd2  17725  catlid  17727  catrid  17728  homffval  17734  homfeqd  17739  homfeqval  17741  comfffval  17742  comffval  17743  comfeq  17750  comfeqd  17751  comfeqval  17752  catpropd  17753  oppcval  17757  oppcco  17762  monfval  17779  ismon  17780  oppcmon  17785  oppcepi  17786  sectffval  17797  sectfval  17798  invffval  17805  isoval  17812  dfiso2  17819  isofn  17822  invisoinvl  17837  invcoisoid  17839  isocoinvid  17840  issubc  17885  issubc3  17899  isfunc  17914  cofuval  17932  cofuval2  17937  funcres  17946  funcres2b  17947  funcres2  17948  idfusubc  17950  funcres2c  17954  isfull  17963  isfth  17967  fullres2c  17992  natfval  18000  isnat  18001  fucval  18013  fucco  18018  fucpropd  18033  initoval  18046  termoval  18047  homarcl  18081  coafval  18117  resssetc  18145  resscatc  18162  catciso  18164  xpcval  18232  1stfval  18246  2ndfval  18249  prfval  18254  prfcl  18258  evlfval  18273  curfval  18279  curf1cl  18284  curfcl  18288  uncf1  18292  uncf2  18293  diag12  18300  diag2  18301  curf2ndf  18303  hofval  18308  hof1  18310  hof2fval  18311  hofcl  18315  yon12  18321  yon2  18322  hofpropd  18323  joinval  18434  meetval  18448  isdlat  18579  plusffval  18671  ismgmd  18677  issstrmgm  18678  grpidval  18686  grpidd  18696  gsumvalx  18701  gsumpropd  18703  gsumress  18707  ismgmhm  18721  issubmgm  18727  resmgmhm  18736  resmgmhm2  18737  resmgmhm2b  18738  issgrpd  18755  ismndd  18781  issubmnd  18786  submnd0  18788  ismhm  18810  issubm  18828  resmhm  18845  resmhm2  18846  resmhm2b  18847  mhmimalem  18849  isgrp  18969  isgrpd2e  18985  grpidd2  19007  grpinvfval  19008  grpinvfvalALT  19009  imasgrp2  19085  imasgrp  19086  subg0  19162  subginv  19163  subgcl  19166  issubgrpd2  19172  isnsg  19185  isghm  19245  isghmOLD  19246  resghm  19262  isga  19321  subgga  19330  gasubg  19332  cntzfval  19350  resscntz  19363  odfval  19564  odfvalALT  19565  gexval  19610  lsmfval  19670  lsmvalx  19671  oppglsm  19674  subglsm  19705  pj1fval  19726  efgtval  19755  iscmn  19821  iscmnd  19826  submcmn2  19871  imasabl  19908  iscyg  19911  cycsubmcmn  19921  prdsmgp  20168  rngpropd  20191  ringurd  20202  issrg  20205  isring  20254  ringidss  20290  mulgass3  20369  dvdsrval  20377  rdivmuldivd  20429  isirred  20435  rnghmval  20456  islring  20556  lringuplu  20560  subrngmcl  20573  subrg1  20598  subrgdvds  20602  subrguss  20603  subrginv  20604  subrgdv  20605  subrgunit  20606  subrgugrp  20607  rnghmresel  20636  rngchom  20639  rngcco  20643  rnghmsubcsetclem1  20647  rhmresel  20665  ringchom  20668  ringcco  20672  rhmsubcsetclem1  20676  rhmsubcrngclem1  20682  rrgval  20713  isdrngd  20781  isdrngrd  20782  isdrngdOLD  20783  isdrngrdOLD  20784  abvfval  20827  isabvd  20829  issrngd  20872  islmod  20878  islmodd  20880  scaffval  20894  lmodpropd  20939  lssset  20948  islssd  20950  prdslmodd  20984  islmhm  21043  reslmhm  21068  reslmhm2  21069  reslmhm2b  21070  islbs  21092  rlmvneg  21230  rnglidlmmgm  21272  rnglidlmsgrp  21273  rnglidlrng  21274  rngqiprngghmlem3  21316  rngqiprngimfolem  21317  rngqiprnglinlem1  21318  rngqiprngimf1  21327  rngqiprnglin  21329  rng2idl1cntr  21332  rngqiprngfulem5  21342  irinitoringc  21507  isphl  21663  ipffval  21683  isphld  21689  phssipval  21692  phssip  21693  phlssphl  21694  ocvfval  21701  isobs  21757  frlmplusgval  21801  frlmsubgval  21802  frlmvscafval  21803  frlmip  21815  frlmipval  21816  frlmup1  21835  lsslindf  21867  isassa  21893  isassad  21902  sraassab  21905  assamulgscmlem2  21937  psrval  21952  resspsradd  22012  resspsrmul  22013  resspsrvsca  22014  mplmon2mul  22110  ply1coe  22317  ply1chr  22325  lply1binomsc  22330  evl1expd  22364  evl1scvarpw  22382  asclply1subcl  22393  mamufval  22411  matplusg2  22448  matvsca2  22449  matplusgcell  22454  matsubgcell  22455  matinvgcell  22456  matvscacell  22457  matmulcell  22466  mpomatmul  22467  mat1  22468  mattposm  22480  mat1dimmul  22497  dmatmul  22518  dmatcrng  22523  scmataddcl  22537  scmatsubcl  22538  scmatcrng  22542  smatvscl  22545  scmatghm  22554  scmatmhm  22555  mvmulfval  22563  ma1repveval  22592  mdetrlin  22623  mdetrsca  22624  mdetmul  22644  madurid  22665  minmar1cl  22672  smadiadetglem1  22692  smadiadetr  22696  matinv  22698  slesolinv  22701  slesolinvbi  22702  cramerimplem3  22706  cpmatacl  22737  mat2pmatghm  22751  decpmatmullem  22792  decpmatmul  22793  pmatcollpw1lem1  22795  pmatcollpw2lem  22798  pmatcollpwlem  22801  pmatcollpw3lem  22804  mply1topmatval  22825  mp2pm2mplem1  22827  mp2pm2mplem4  22830  mp2pm2mplem5  22831  mp2pm2mp  22832  chpmat1d  22857  chpscmatgsummon  22866  chfacfpmmulgsum2  22886  xkocnv  23837  submtmd  24127  prdsdsf  24392  ressprdsds  24396  blfvalps  24408  prdsxmslem2  24557  tmsxpsval  24566  ngpds  24632  sgrimval  24660  subgngp  24663  tngngp  24690  tngngp3  24692  isnlm  24711  lssnlm  24737  isphtpy  25026  isphtpc  25039  pi1cpbl  25090  pi1addf  25093  pi1addval  25094  pi1grplem  25095  clmsub  25126  clmvsass  25135  clmvsdir  25137  isclmp  25143  cvsdiv  25178  iscph  25217  cphdir  25252  cphdi  25253  cph2di  25254  cph2subdi  25257  cphass  25258  tcphval  25265  ipcau2  25281  tcphcphlem1  25282  tcphcphlem2  25283  cphsscph  25298  caufval  25322  rrxip  25437  rrxvsca  25441  rrxplusgvscavalb  25442  rrxdsfival  25460  ehleudisval  25466  dvlip2  26048  q1pval  26208  r1pval  26211  dvntaylp  26427  efabl  26606  efsubm  26607  dchrmul  27306  seqseq123d  28306  istrkgc  28476  istrkgb  28477  istrkgcb  28478  istrkge  28479  istrkgl  28480  istrkgld  28481  iscgrg  28534  isismt  28556  tglngval  28573  legval  28606  ishlg  28624  mirval  28677  israg  28719  ishpg  28781  lmif  28807  islmib  28809  isinag  28860  ttgval  28897  ttgvalOLD  28898  wksonproplem  29736  wksonproplemOLD  29737  wspthsnon  29881  iswwlksnon  29882  iswspthsnon  29885  isconngr  30217  isconngr1  30218  grpodivval  30563  dipfval  30730  ipval  30731  sspgval  30757  sspsval  30759  lnoval  30780  ajfval  30837  dipdir  30870  dipass  30873  htth  30946  isomnd  33060  submomnd  33069  inftmrel  33169  isinftm  33170  isslmd  33190  elrgspnlem1  33231  erlval  33244  rlocval  33245  rlocaddval  33254  rlocmulval  33255  subrdom  33268  isorng  33308  suborng  33324  resv1r  33347  lsmidllsp  33407  idlinsubrg  33438  prmidlval  33444  idlsrgval  33510  idlsrg0g  33513  rprmval  33523  drgextlsp  33622  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  extdg1id  33690  algextdeglem8  33729  smatlem  33757  submatminr1  33770  metidval  33850  pstmval  33855  pstmfval  33856  zlm0  33920  zlm1  33921  sitmval  34330  breprexp  34626  istrkg2d  34659  afsval  34664  mclsrcl  35545  mppsval  35556  bj-endval  37297  matunitlindflem2  37603  istotbnd  37755  isbnd  37766  rrnequiv  37821  isrngo  37883  rngohomval  37950  idlval  37999  pridlval  38019  lflset  39040  islfld  39043  ldualvadd  39110  ldualsmul  39116  ldualvs  39118  isopos  39161  cmtfvalN  39191  iscvlat  39304  ishlat1  39333  lineset  39720  psubspset  39726  paddfval  39779  paddval  39780  ltrnfset  40099  trnfsetN  40137  trlfset  40142  tgrpov  40730  erngplus  40785  erngmul  40788  erngplus-rN  40793  erngmul-rN  40796  erngdvlem3  40972  erngdvlem4  40973  erng0g  40976  erngdvlem3-rN  40980  erngdvlem4-rN  40981  dvaplusg  40991  dvamulr  40994  dvavadd  40997  dvavsca  40999  dvalveclem  41007  dvhmulr  41068  dvhfvadd  41073  dvhvadd  41074  dvhopvadd2  41076  dvhvaddcl  41077  dvhvaddcomN  41078  dvhvsca  41083  dvhlveclem  41090  dvh0g  41093  djavalN  41117  diblsmopel  41153  dicvaddcl  41172  cdlemn6  41184  dihffval  41212  dihopelvalcpre  41230  djhval  41380  lcdvaddval  41580  lcdsmul  41584  lcdvsval  41586  lcdlkreq2N  41605  hvmapffval  41740  hvmapfval  41741  hdmap1fval  41778  hgmapffval  41867  hgmapfval  41868  hgmapadd  41876  hlhilipval  41935  hlhilhillem  41946  isprimroot  42074  aks6d1c1p4  42092  idomnnzpownz  42113  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks5lem3a  42170  unitscyglem5  42180  rhmpsr1  42539  selvvvval  42571  mhphf2  42584  prjspval  42589  prjspner1  42612  sn-isghm  42659  mnringvald  44203  ioorrnopnlem  46259  hoidmvval0b  46545  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvle  46555  ovnhoi  46558  hoiqssbl  46580  hspmbllem2  46582  vonioo  46637  vonicc  46640  zlidlring  48077  uzlidlring  48078  ovmpordxf  48183  lincop  48253  lincval  48254  lincsum  48274  lincscm  48275  lmod1lem2  48333  lmod1lem3  48334  lmod1lem4  48335  ldepsnlinc  48353  lines  48580  line  48581  rrxlines  48582  rrxline  48583  spheres  48595  fvconstr  48685  fvconstrn0  48686  fvconstr2  48687  catprs  48799  thincmod  48830  isthincd2lem2  48835  isthincd  48836  mndtcco2  48894  mndtccatid  48895  oppgoppchom  48898  oppgoppcco  48899  grptcmon  48901  grptcepi  48902