Theorem oveqd 7433

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 7422	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveq123d  7437  oveqdr  7444  csbov  7461  csbov12g  7462  ovmpodxf  7566  oprssov  7586  2mpo0  7666  ofeqd  7683  mptmpoopabbrd  8083  mptmpoopabovd  8084  el2mpocsbcl  8085  fnmpoovd  8087  frecseq123  8284  ruclem1  16323  vdwapval  17069  vdwapid1  17071  vdwmc2  17075  vdwpc  17076  vdwlem5  17081  vdwlem8  17084  vdwlem13  17089  prdsval  17544  prdsdsval2  17573  pwsplusgval  17580  pwsmulrval  17581  pwsvscafval  17584  imasval  17601  iscat  17764  iscatd  17765  catidex  17766  catideu  17767  cidfval  17768  cidval  17769  catidd  17772  iscatd2  17773  catlid  17775  catrid  17776  homffval  17782  homfeqd  17787  homfeqval  17789  comfffval  17790  comffval  17791  comfeq  17798  comfeqd  17799  comfeqval  17800  catpropd  17801  oppcval  17805  oppcco  17809  monfval  17825  ismon  17826  oppcmon  17831  oppcepi  17832  sectffval  17843  sectfval  17844  invffval  17851  isoval  17858  dfiso2  17865  isofn  17868  invisoinvl  17883  invcoisoid  17885  isocoinvid  17886  issubc  17928  issubc3  17942  isfunc  17957  cofuval  17975  cofuval2  17980  funcres  17989  funcres2b  17990  funcres2  17991  idfusubc  17993  funcres2c  17996  isfull  18005  isfth  18009  fullres2c  18034  natfval  18042  isnat  18043  fucval  18054  fucco  18058  fucpropd  18073  initoval  18086  termoval  18087  homarcl  18121  coafval  18157  resssetc  18185  resscatc  18202  catciso  18204  xpcval  18269  1stfval  18283  2ndfval  18286  prfval  18291  prfcl  18295  evlfval  18309  curfval  18315  curf1cl  18320  curfcl  18324  uncf1  18328  uncf2  18329  diag12  18336  diag2  18337  curf2ndf  18339  hofval  18344  hof1  18346  hof2fval  18347  hofcl  18351  yon12  18357  yon2  18358  hofpropd  18359  joinval  18467  meetval  18481  isdlat  18614  plusffval  18740  ismgmd  18748  issstrmgm  18749  grpidval  18758  grpidd  18769  idressid  18779  gsumvalx  18780  gsumpropd  18782  gsumress  18786  ismgmhm  18800  issubmgm  18806  resmgmhm  18815  resmgmhm2  18816  resmgmhm2b  18817  issgrpd  18834  ismndd  18861  issubmnd  18868  submnd0OLD  18872  ismhm  18894  issubm  18912  resmhm  18930  resmhm2  18931  resmhm2b  18932  mhmimalem  18934  isgrp  19064  isgrpd2e  19080  grpidd2  19102  grpinvfval  19103  grpinvfvalALT  19104  imasgrp2  19179  imasgrp  19180  subg0  19256  subginv  19257  subgcl  19260  issubgrpd2  19267  isnsg  19279  isghm  19344  resghm  19360  isga  19419  subgga  19428  gasubg  19430  cntzfval  19448  resscntz  19461  odfval  19660  odfvalALT  19661  gexval  19706  lsmfval  19766  lsmvalx  19767  oppglsm  19770  subglsm  19801  pj1fval  19822  efgtval  19851  iscmn  19917  iscmnd  19922  submcmn2  19967  imasabl  20004  iscyg  20007  cycsubmcmn  20017  isomnd  20251  submomnd  20260  prdsmgp  20285  rngpropd  20310  ringurd  20325  issrg  20328  isring  20377  ringidss  20419  mulgass3  20495  dvdsrval  20503  rdivmuldivd  20555  isirred  20561  rnghmval  20582  rhmval0  20617  islring  20703  lringuplu  20707  subrngmcl  20720  subrg1  20745  subrgdvds  20749  subrguss  20750  subrginv  20751  subrgdv  20752  subrgunit  20753  subrgugrp  20754  rnghmresel  20783  rngchom  20786  rngcco  20790  rnghmsubcsetclem1  20794  rhmresel  20812  ringchom  20815  ringcco  20819  rhmsubcsetclem1  20823  rhmsubcrngclem1  20829  rrgval  20860  isdrngd  20932  isdrngrd  20933  isdrngdOLD  20934  isdrngrdOLD  20935  abvfval  20977  isabvd  20979  issrngd  21022  isorng  21028  suborng  21043  islmod  21049  islmodd  21051  scaffval  21065  lmodpropd  21110  lssset  21118  islssd  21120  prdslmodd  21154  islmhm  21212  reslmhm  21237  reslmhm2  21238  reslmhm2b  21239  islbs  21261  rlmvneg  21391  rnglidlmmgm  21443  rnglidlmsgrp  21444  rnglidlrng  21445  lsmidllsp  21447  rngqiprngghmlem3  21493  rngqiprngimfolem  21494  rngqiprnglinlem1  21495  rngqiprngimf1  21504  rngqiprnglin  21506  rng2idl1cntr  21509  rngqiprngfulem5  21519  prmidlval  21526  irinitoringc  21693  isphl  21842  ipffval  21862  isphld  21868  phssipval  21871  phssip  21872  phlssphl  21873  ocvfval  21880  isobs  21934  frlmplusgval  21978  frlmsubgval  21979  frlmvscafval  21980  frlmip  21992  frlmipval  21993  frlmup1  22012  lsslindf  22044  isassa  22072  isassad  22081  sraassab  22084  assamulgscmlem2  22116  psrval  22131  resspsradd  22190  resspsrmul  22191  resspsrvsca  22192  mplmon2mul  22286  selvvvval  22359  ply1coe  22524  ply1chr  22532  lply1binomsc  22537  evl1expd  22571  evl1scvarpw  22589  asclply1subcl  22600  mamufval  22615  matplusg2  22650  matvsca2  22651  matplusgcell  22656  matsubgcell  22657  matinvgcell  22658  matvscacell  22659  matmulcell  22668  mpomatmul  22669  mat1  22670  mattposm  22682  mat1dimmul  22699  dmatmul  22720  dmatcrng  22725  scmataddcl  22739  scmatsubcl  22740  scmatcrng  22744  smatvscl  22747  scmatghm  22756  scmatmhm  22757  mvmulfval  22765  ma1repveval  22794  mdetrlin  22825  mdetrsca  22826  mdetmul  22846  madurid  22867  minmar1cl  22874  smadiadetglem1  22894  smadiadetr  22898  matinv  22900  matunitlindflem2  22903  slesolinv  22906  slesolinvbi  22907  cramerimplem3  22911  cpmatacl  22942  mat2pmatghm  22956  decpmatmullem  22997  decpmatmul  22998  pmatcollpw1lem1  23000  pmatcollpw2lem  23003  pmatcollpwlem  23006  pmatcollpw3lem  23009  mply1topmatval  23030  mp2pm2mplem1  23032  mp2pm2mplem4  23035  mp2pm2mplem5  23036  mp2pm2mp  23037  chpmat1d  23062  chpscmatgsummon  23071  chfacfpmmulgsum2  23091  xkocnv  24041  submtmd  24331  prdsdsf  24594  ressprdsds  24598  blfvalps  24610  prdsxmslem2  24756  tmsxpsval  24765  ngpds  24831  sgrimval  24859  subgngp  24862  tngngp  24881  tngngp3  24883  isnlm  24902  lssnlm  24928  isphtpy  25210  isphtpc  25223  pi1cpbl  25273  pi1addf  25276  pi1addval  25277  pi1grplem  25278  clmsub  25309  clmvsass  25318  clmvsdir  25320  isclmp  25326  cvsdiv  25361  iscph  25399  cphdir  25434  cphdi  25435  cph2di  25436  cph2subdi  25439  cphass  25440  tcphval  25447  ipcau2  25463  tcphcphlem1  25464  tcphcphlem2  25465  cphsscph  25480  caufval  25504  rrxip  25619  rrxvsca  25623  rrxplusgvscavalb  25624  rrxdsfival  25642  ehleudisval  25648  dvlip2  26224  q1pval  26382  r1pval  26385  dvntaylp  26604  efabl  26785  efsubm  26786  dchrmul  27482  seqseq123d  28549  istrkgc  28793  istrkgb  28794  istrkgcb  28795  istrkge  28796  istrkgl  28797  istrkgld  28798  iscgrg  28852  isismt  28874  tglngval  28891  legval  28924  ishlg2  28942  ishlg  28945  mirval  29004  israg  29049  ishpg  29114  tgplnfn  29130  plngval  29132  isplng  29133  lmif  29167  islmib  29169  isinag  29234  ttgval  29317  wksonproplem  30152  wspthsnon  30306  iswwlksnon  30307  iswspthsnon  30310  isconngr  30655  isconngr1  30656  grpodivval  31002  dipfval  31169  ipval  31170  sspgval  31196  sspsval  31198  lnoval  31219  ajfval  31276  dipdir  31309  dipass  31312  htth  31385  ressmulgnn0d  33471  inftmrel  33607  isinftm  33608  isslmd  33629  elrgspnlem1  33669  erlval  33685  rlocval  33686  rlocaddval  33696  rlocmulval  33697  subrdom  33712  resv1r  33766  idlinsubrg  33846  idlsrgval  33900  idlsrg0g  33903  rprmval  33913  ressply1evls1  33962  vietalem  34076  drgextlsp  34091  fedgmullem1  34126  fedgmullem2  34127  fedgmul  34128  extdg1id  34163  fldextrspunlsplem  34170  fldextrspunlsp  34171  extdgfialglem1  34189  extdgfialglem2  34190  algextdeglem8  34221  smatlem  34294  submatminr1  34307  metidval  34387  pstmval  34392  pstmfval  34393  zlm0  34457  zlm1  34458  sitmval  34847  breprexp  35128  istrkg2d  35161  afsval  35169  mclsrcl  36127  mppsval  36138  bj-endval  38054  istotbnd  38506  isbnd  38517  rrnequiv  38572  isrngo  38634  rngohomval  38701  idlval  38750  pridlval  38770  lflset  39919  islfld  39922  ldualvadd  39989  ldualsmul  39995  ldualvs  39997  isopos  40040  cmtfvalN  40070  iscvlat  40183  ishlat1  40212  lineset  40598  psubspset  40604  paddfval  40657  paddval  40658  ltrnfset  40977  trnfsetN  41015  trlfset  41020  tgrpov  41608  erngplus  41663  erngmul  41666  erngplus-rN  41671  erngmul-rN  41674  erngdvlem3  41850  erngdvlem4  41851  erng0g  41854  erngdvlem3-rN  41858  erngdvlem4-rN  41859  dvaplusg  41869  dvamulr  41872  dvavadd  41875  dvavsca  41877  dvalveclem  41885  dvhmulr  41946  dvhfvadd  41951  dvhvadd  41952  dvhopvadd2  41954  dvhvaddcl  41955  dvhvaddcomN  41956  dvhvsca  41961  dvhlveclem  41968  dvh0g  41971  djavalN  41995  diblsmopel  42031  dicvaddcl  42050  cdlemn6  42062  dihffval  42090  dihopelvalcpre  42108  djhval  42258  lcdvaddval  42458  lcdsmul  42462  lcdvsval  42464  lcdlkreq2N  42483  hvmapffval  42618  hvmapfval  42619  hdmap1fval  42656  hgmapffval  42745  hgmapfval  42746  hgmapadd  42754  hlhilipval  42809  hlhilhillem  42820  isprimroot  42946  aks6d1c1p4  42964  idomnnzpownz  42985  aks6d1c5lem1  42989  aks6d1c5lem3  42990  aks6d1c5lem2  42991  aks5lem3a  43042  unitscyglem5  43052  rhmpsr1  43417  mhphf2  43431  prjspval  43436  prjspner1  43459  sn-isghm  43506  mnringvald  45038  ioorrnopnlem  47119  hoidmvval0b  47405  hoidmvlelem2  47411  hoidmvlelem3  47412  hoidmvle  47415  ovnhoi  47418  hoiqssbl  47440  hspmbllem2  47442  vonioo  47497  vonicc  47500  zlidlring  49136  uzlidlring  49137  ovmpordxf  49256  lincop  49325  lincval  49326  lincsum  49346  lincscm  49347  lmod1lem2  49405  lmod1lem3  49406  lmod1lem4  49407  ldepsnlinc  49425  lines  49648  line  49649  rrxlines  49650  rrxline  49651  spheres  49663  fvconstr  49777  fvconstrn0  49778  fvconstr2  49779  catprs  49924  sectrcl2  49936  invrcl2  49938  invfn  49943  isorcl2  49947  sectpropdlem  49949  invpropdlem  49951  isopropdlem  49953  cicpropdlem  49962  iinfconstbas  49979  nelsubclem  49980  nelsubc3lem  49983  ssccatid  49985  resccatlem  49986  cofu2a  50008  cofid2a  50026  cofid2  50028  cofidf2a  50030  cofidf2  50033  oppf2  50053  upfval  50089  upfval2  50090  upfval3  50091  upeu3  50108  upeu4  50109  oppcup3  50122  natoppfb  50144  swapfval  50175  swapf2a  50184  1stfpropd  50203  2ndfpropd  50204  cofuswapf2  50208  tposcurf12  50211  tposcurf2  50213  tposcurf2cl  50215  fucofvalg  50231  fuco11b  50250  fuco23a  50265  precofval3  50284  prcofpropd  50292  catcrcl2  50309  opf12  50317  fucoppcco  50322  thincmod  50343  isthincd2lem2  50348  isthincd  50349  dfinito4  50414  mndtcco2  50499  mndtccatid  50500  oppgoppchom  50503  oppgoppcco  50504  grptcmon  50506  grptcepi  50507  2arwcatlem2  50509  2arwcatlem3  50510  2arwcatlem4  50511  2arwcat  50513  lanrcl  50534  ranrcl  50535  rellan  50536  relran  50537  concom  50576  coccom  50577