Theorem oveqd 7420

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  oveq123d  7424  oveqdr  7431  csbov  7448  csbov12g  7449  ovmpodxf  7555  oprssov  7574  2mpo0  7654  ofeqd  7671  mptmpoopabbrd  8077  mptmpoopabbrdOLD  8078  mptmpoopabovd  8079  mptmpoopabbrdOLDOLD  8080  mptmpoopabovdOLD  8081  el2mpocsbcl  8082  fnmpoovd  8084  frecseq123  8279  ruclem1  16247  vdwapval  16991  vdwapid1  16993  vdwmc2  16997  vdwpc  16998  vdwlem5  17003  vdwlem8  17006  vdwlem13  17011  prdsval  17467  prdsdsval2  17496  pwsplusgval  17502  pwsmulrval  17503  pwsvscafval  17506  imasval  17523  iscat  17682  iscatd  17683  catidex  17684  catideu  17685  cidfval  17686  cidval  17687  catidd  17690  iscatd2  17691  catlid  17693  catrid  17694  homffval  17700  homfeqd  17705  homfeqval  17707  comfffval  17708  comffval  17709  comfeq  17716  comfeqd  17717  comfeqval  17718  catpropd  17719  oppcval  17723  oppcco  17727  monfval  17743  ismon  17744  oppcmon  17749  oppcepi  17750  sectffval  17761  sectfval  17762  invffval  17769  isoval  17776  dfiso2  17783  isofn  17786  invisoinvl  17801  invcoisoid  17803  isocoinvid  17804  issubc  17846  issubc3  17860  isfunc  17875  cofuval  17893  cofuval2  17898  funcres  17907  funcres2b  17908  funcres2  17909  idfusubc  17911  funcres2c  17914  isfull  17923  isfth  17927  fullres2c  17952  natfval  17960  isnat  17961  fucval  17972  fucco  17976  fucpropd  17991  initoval  18004  termoval  18005  homarcl  18039  coafval  18075  resssetc  18103  resscatc  18120  catciso  18122  xpcval  18187  1stfval  18201  2ndfval  18204  prfval  18209  prfcl  18213  evlfval  18227  curfval  18233  curf1cl  18238  curfcl  18242  uncf1  18246  uncf2  18247  diag12  18254  diag2  18255  curf2ndf  18257  hofval  18262  hof1  18264  hof2fval  18265  hofcl  18269  yon12  18275  yon2  18276  hofpropd  18277  joinval  18385  meetval  18399  isdlat  18530  plusffval  18622  ismgmd  18628  issstrmgm  18629  grpidval  18637  grpidd  18647  gsumvalx  18652  gsumpropd  18654  gsumress  18658  ismgmhm  18672  issubmgm  18678  resmgmhm  18687  resmgmhm2  18688  resmgmhm2b  18689  issgrpd  18706  ismndd  18732  issubmnd  18737  submnd0  18739  ismhm  18761  issubm  18779  resmhm  18796  resmhm2  18797  resmhm2b  18798  mhmimalem  18800  isgrp  18920  isgrpd2e  18936  grpidd2  18958  grpinvfval  18959  grpinvfvalALT  18960  imasgrp2  19036  imasgrp  19037  subg0  19113  subginv  19114  subgcl  19117  issubgrpd2  19123  isnsg  19136  isghm  19196  isghmOLD  19197  resghm  19213  isga  19272  subgga  19281  gasubg  19283  cntzfval  19301  resscntz  19314  odfval  19511  odfvalALT  19512  gexval  19557  lsmfval  19617  lsmvalx  19618  oppglsm  19621  subglsm  19652  pj1fval  19673  efgtval  19702  iscmn  19768  iscmnd  19773  submcmn2  19818  imasabl  19855  iscyg  19858  cycsubmcmn  19868  prdsmgp  20109  rngpropd  20132  ringurd  20143  issrg  20146  isring  20195  ringidss  20235  mulgass3  20311  dvdsrval  20319  rdivmuldivd  20371  isirred  20377  rnghmval  20398  islring  20498  lringuplu  20502  subrngmcl  20515  subrg1  20540  subrgdvds  20544  subrguss  20545  subrginv  20546  subrgdv  20547  subrgunit  20548  subrgugrp  20549  rnghmresel  20578  rngchom  20581  rngcco  20585  rnghmsubcsetclem1  20589  rhmresel  20607  ringchom  20610  ringcco  20614  rhmsubcsetclem1  20618  rhmsubcrngclem1  20624  rrgval  20655  isdrngd  20723  isdrngrd  20724  isdrngdOLD  20725  isdrngrdOLD  20726  abvfval  20768  isabvd  20770  issrngd  20813  islmod  20819  islmodd  20821  scaffval  20835  lmodpropd  20880  lssset  20888  islssd  20890  prdslmodd  20924  islmhm  20983  reslmhm  21008  reslmhm2  21009  reslmhm2b  21010  islbs  21032  rlmvneg  21162  rnglidlmmgm  21204  rnglidlmsgrp  21205  rnglidlrng  21206  rngqiprngghmlem3  21248  rngqiprngimfolem  21249  rngqiprnglinlem1  21250  rngqiprngimf1  21259  rngqiprnglin  21261  rng2idl1cntr  21264  rngqiprngfulem5  21274  irinitoringc  21438  isphl  21586  ipffval  21606  isphld  21612  phssipval  21615  phssip  21616  phlssphl  21617  ocvfval  21624  isobs  21678  frlmplusgval  21722  frlmsubgval  21723  frlmvscafval  21724  frlmip  21736  frlmipval  21737  frlmup1  21756  lsslindf  21788  isassa  21814  isassad  21823  sraassab  21826  assamulgscmlem2  21858  psrval  21873  resspsradd  21933  resspsrmul  21934  resspsrvsca  21935  mplmon2mul  22025  ply1coe  22234  ply1chr  22242  lply1binomsc  22247  evl1expd  22281  evl1scvarpw  22299  asclply1subcl  22310  mamufval  22328  matplusg2  22363  matvsca2  22364  matplusgcell  22369  matsubgcell  22370  matinvgcell  22371  matvscacell  22372  matmulcell  22381  mpomatmul  22382  mat1  22383  mattposm  22395  mat1dimmul  22412  dmatmul  22433  dmatcrng  22438  scmataddcl  22452  scmatsubcl  22453  scmatcrng  22457  smatvscl  22460  scmatghm  22469  scmatmhm  22470  mvmulfval  22478  ma1repveval  22507  mdetrlin  22538  mdetrsca  22539  mdetmul  22559  madurid  22580  minmar1cl  22587  smadiadetglem1  22607  smadiadetr  22611  matinv  22613  slesolinv  22616  slesolinvbi  22617  cramerimplem3  22621  cpmatacl  22652  mat2pmatghm  22666  decpmatmullem  22707  decpmatmul  22708  pmatcollpw1lem1  22710  pmatcollpw2lem  22713  pmatcollpwlem  22716  pmatcollpw3lem  22719  mply1topmatval  22740  mp2pm2mplem1  22742  mp2pm2mplem4  22745  mp2pm2mplem5  22746  mp2pm2mp  22747  chpmat1d  22772  chpscmatgsummon  22781  chfacfpmmulgsum2  22801  xkocnv  23750  submtmd  24040  prdsdsf  24304  ressprdsds  24308  blfvalps  24320  prdsxmslem2  24466  tmsxpsval  24475  ngpds  24541  sgrimval  24569  subgngp  24572  tngngp  24591  tngngp3  24593  isnlm  24612  lssnlm  24638  isphtpy  24929  isphtpc  24942  pi1cpbl  24993  pi1addf  24996  pi1addval  24997  pi1grplem  24998  clmsub  25029  clmvsass  25038  clmvsdir  25040  isclmp  25046  cvsdiv  25081  iscph  25120  cphdir  25155  cphdi  25156  cph2di  25157  cph2subdi  25160  cphass  25161  tcphval  25168  ipcau2  25184  tcphcphlem1  25185  tcphcphlem2  25186  cphsscph  25201  caufval  25225  rrxip  25340  rrxvsca  25344  rrxplusgvscavalb  25345  rrxdsfival  25363  ehleudisval  25369  dvlip2  25950  q1pval  26110  r1pval  26113  dvntaylp  26329  efabl  26509  efsubm  26510  dchrmul  27209  seqseq123d  28209  istrkgc  28379  istrkgb  28380  istrkgcb  28381  istrkge  28382  istrkgl  28383  istrkgld  28384  iscgrg  28437  isismt  28459  tglngval  28476  legval  28509  ishlg  28527  mirval  28580  israg  28622  ishpg  28684  lmif  28710  islmib  28712  isinag  28763  ttgval  28800  wksonproplem  29630  wksonproplemOLD  29631  wspthsnon  29780  iswwlksnon  29781  iswspthsnon  29784  isconngr  30116  isconngr1  30117  grpodivval  30462  dipfval  30629  ipval  30630  sspgval  30656  sspsval  30658  lnoval  30679  ajfval  30736  dipdir  30769  dipass  30772  htth  30845  ressmulgnn0d  32985  isomnd  33015  submomnd  33024  inftmrel  33124  isinftm  33125  isslmd  33145  elrgspnlem1  33183  erlval  33199  rlocval  33200  rlocaddval  33209  rlocmulval  33210  subrdom  33225  isorng  33267  suborng  33283  resv1r  33301  lsmidllsp  33361  idlinsubrg  33392  prmidlval  33398  idlsrgval  33464  idlsrg0g  33467  rprmval  33477  ressply1evls1  33524  drgextlsp  33579  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  extdg1id  33653  fldextrspunlsplem  33660  fldextrspunlsp  33661  algextdeglem8  33704  smatlem  33774  submatminr1  33787  metidval  33867  pstmval  33872  pstmfval  33873  zlm0  33937  zlm1  33938  sitmval  34327  breprexp  34611  istrkg2d  34644  afsval  34649  mclsrcl  35529  mppsval  35540  bj-endval  37279  matunitlindflem2  37587  istotbnd  37739  isbnd  37750  rrnequiv  37805  isrngo  37867  rngohomval  37934  idlval  37983  pridlval  38003  lflset  39023  islfld  39026  ldualvadd  39093  ldualsmul  39099  ldualvs  39101  isopos  39144  cmtfvalN  39174  iscvlat  39287  ishlat1  39316  lineset  39703  psubspset  39709  paddfval  39762  paddval  39763  ltrnfset  40082  trnfsetN  40120  trlfset  40125  tgrpov  40713  erngplus  40768  erngmul  40771  erngplus-rN  40776  erngmul-rN  40779  erngdvlem3  40955  erngdvlem4  40956  erng0g  40959  erngdvlem3-rN  40963  erngdvlem4-rN  40964  dvaplusg  40974  dvamulr  40977  dvavadd  40980  dvavsca  40982  dvalveclem  40990  dvhmulr  41051  dvhfvadd  41056  dvhvadd  41057  dvhopvadd2  41059  dvhvaddcl  41060  dvhvaddcomN  41061  dvhvsca  41066  dvhlveclem  41073  dvh0g  41076  djavalN  41100  diblsmopel  41136  dicvaddcl  41155  cdlemn6  41167  dihffval  41195  dihopelvalcpre  41213  djhval  41363  lcdvaddval  41563  lcdsmul  41567  lcdvsval  41569  lcdlkreq2N  41588  hvmapffval  41723  hvmapfval  41724  hdmap1fval  41761  hgmapffval  41850  hgmapfval  41851  hgmapadd  41859  hlhilipval  41914  hlhilhillem  41925  isprimroot  42052  aks6d1c1p4  42070  idomnnzpownz  42091  aks6d1c5lem1  42095  aks6d1c5lem3  42096  aks6d1c5lem2  42097  aks5lem3a  42148  unitscyglem5  42158  rhmpsr1  42523  selvvvval  42555  mhphf2  42568  prjspval  42573  prjspner1  42596  sn-isghm  42643  mnringvald  44185  ioorrnopnlem  46281  hoidmvval0b  46567  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvle  46577  ovnhoi  46580  hoiqssbl  46602  hspmbllem2  46604  vonioo  46659  vonicc  46662  zlidlring  48157  uzlidlring  48158  ovmpordxf  48262  lincop  48332  lincval  48333  lincsum  48353  lincscm  48354  lmod1lem2  48412  lmod1lem3  48413  lmod1lem4  48414  ldepsnlinc  48432  lines  48659  line  48660  rrxlines  48661  rrxline  48662  spheres  48674  fvconstr  48786  fvconstrn0  48787  fvconstr2  48788  catprs  48934  invfn  48948  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955  cicpropdlem  48964  iinfconstbas  48981  nelsubclem  48982  nelsubc3lem  48985  ssccatid  48987  resccatlem  48988  upfval  49059  upfval2  49060  upfval3  49061  upeu3  49076  upeu4  49077  oppcup3  49090  swapfval  49127  swapf2a  49136  cofuswapf2  49154  tposcurf12  49157  tposcurf2  49159  tposcurf2cl  49161  fucofvalg  49177  fuco11b  49196  fuco23a  49211  precofval3  49230  thincmod  49264  isthincd2lem2  49269  isthincd  49270  dfinito4  49334  mndtcco2  49411  mndtccatid  49412  oppgoppchom  49415  oppgoppcco  49416  grptcmon  49418  grptcepi  49419  2arwcatlem2  49421  2arwcatlem3  49422  2arwcatlem4  49423  2arwcat  49425  lanrcl  49444  ranrcl  49445  rellan  49446  relran  49447  concom  49481  coccom  49482