Theorem oveqd 7426

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  oveq123d  7430  oveqdr  7437  csbov  7452  csbov12g  7453  ovmpodxf  7558  oprssov  7576  2mpo0  7655  ofeqd  7672  mptmpoopabbrd  8067  mptmpoopabovd  8068  mptmpoopabbrdOLD  8069  mptmpoopabovdOLD  8070  el2mpocsbcl  8071  fnmpoovd  8073  frecseq123  8267  ruclem1  16174  vdwapval  16906  vdwapid1  16908  vdwmc2  16912  vdwpc  16913  vdwlem5  16918  vdwlem8  16921  vdwlem13  16926  prdsval  17401  prdsdsval2  17430  pwsplusgval  17436  pwsmulrval  17437  pwsvscafval  17440  imasval  17457  iscat  17616  iscatd  17617  catidex  17618  catideu  17619  cidfval  17620  cidval  17621  catidd  17624  iscatd2  17625  catlid  17627  catrid  17628  homffval  17634  homfeqd  17639  homfeqval  17641  comfffval  17642  comffval  17643  comfeq  17650  comfeqd  17651  comfeqval  17652  catpropd  17653  oppcval  17657  oppcco  17662  monfval  17679  ismon  17680  oppcmon  17685  oppcepi  17686  sectffval  17697  sectfval  17698  invffval  17705  isoval  17712  dfiso2  17719  isofn  17722  invisoinvl  17737  invcoisoid  17739  isocoinvid  17740  issubc  17785  issubc3  17799  isfunc  17814  cofuval  17832  cofuval2  17837  funcres  17846  funcres2b  17847  funcres2  17848  funcres2c  17852  isfull  17861  isfth  17865  fullres2c  17890  natfval  17897  isnat  17898  fucval  17910  fucco  17915  fucpropd  17930  initoval  17943  termoval  17944  homarcl  17978  coafval  18014  resssetc  18042  resscatc  18059  catciso  18061  xpcval  18129  1stfval  18143  2ndfval  18146  prfval  18151  prfcl  18155  evlfval  18170  curfval  18176  curf1cl  18181  curfcl  18185  uncf1  18189  uncf2  18190  diag12  18197  diag2  18198  curf2ndf  18200  hofval  18205  hof1  18207  hof2fval  18208  hofcl  18212  yon12  18218  yon2  18219  hofpropd  18220  joinval  18330  meetval  18344  isdlat  18475  plusffval  18567  issstrmgm  18572  grpidval  18580  grpidd  18590  gsumvalx  18595  gsumpropd  18597  gsumress  18601  issgrpd  18621  ismndd  18647  issubmnd  18652  submnd0  18654  ismhm  18673  issubm  18684  resmhm  18701  resmhm2  18702  resmhm2b  18703  mhmimalem  18705  isgrp  18825  isgrpd2e  18841  grpidd2  18862  grpinvfval  18863  grpinvfvalALT  18864  imasgrp2  18938  imasgrp  18939  subg0  19012  subginv  19013  subgcl  19016  issubgrpd2  19022  isnsg  19035  isghm  19092  resghm  19108  isga  19155  subgga  19164  gasubg  19166  cntzfval  19184  resscntz  19197  odfval  19400  odfvalALT  19401  gexval  19446  lsmfval  19506  lsmvalx  19507  oppglsm  19510  subglsm  19541  pj1fval  19562  efgtval  19591  iscmn  19657  iscmnd  19662  submcmn2  19707  imasabl  19744  iscyg  19747  cycsubmcmn  19757  ringurd  20008  issrg  20011  isring  20060  ringidss  20094  prdsmgp  20132  mulgass3  20167  dvdsrval  20175  rdivmuldivd  20227  isirred  20233  islring  20310  lringuplu  20314  subrg1  20329  subrgmcl  20331  subrgdvds  20333  subrguss  20334  subrginv  20335  subrgdv  20336  subrgunit  20337  subrgugrp  20338  isdrngd  20390  isdrngrd  20391  isdrngdOLD  20392  isdrngrdOLD  20393  abvfval  20426  isabvd  20428  issrngd  20469  islmod  20475  islmodd  20477  scaffval  20490  lmodpropd  20535  lssset  20544  islssd  20546  prdslmodd  20580  islmhm  20638  reslmhm  20663  reslmhm2  20664  reslmhm2b  20665  islbs  20687  rlmvneg  20830  rrgval  20903  isphl  21181  ipffval  21201  isphld  21207  phssipval  21210  phssip  21211  phlssphl  21212  ocvfval  21219  isobs  21275  frlmplusgval  21319  frlmsubgval  21320  frlmvscafval  21321  frlmip  21333  frlmipval  21334  frlmup1  21353  lsslindf  21385  isassa  21411  isassad  21419  sraassab  21422  assamulgscmlem2  21454  psrval  21468  resspsradd  21536  resspsrmul  21537  resspsrvsca  21538  mplmon2mul  21630  ply1coe  21820  lply1binomsc  21831  evl1expd  21864  evl1scvarpw  21882  mamufval  21887  matplusg2  21929  matvsca2  21930  matplusgcell  21935  matsubgcell  21936  matinvgcell  21937  matvscacell  21938  matmulcell  21947  mpomatmul  21948  mat1  21949  mattposm  21961  mat1dimmul  21978  dmatmul  21999  dmatcrng  22004  scmataddcl  22018  scmatsubcl  22019  scmatcrng  22023  smatvscl  22026  scmatghm  22035  scmatmhm  22036  mvmulfval  22044  ma1repveval  22073  mdetrlin  22104  mdetrsca  22105  mdetmul  22125  madurid  22146  minmar1cl  22153  smadiadetglem1  22173  smadiadetr  22177  matinv  22179  slesolinv  22182  slesolinvbi  22183  cramerimplem3  22187  cpmatacl  22218  mat2pmatghm  22232  decpmatmullem  22273  decpmatmul  22274  pmatcollpw1lem1  22276  pmatcollpw2lem  22279  pmatcollpwlem  22282  pmatcollpw3lem  22285  mply1topmatval  22306  mp2pm2mplem1  22308  mp2pm2mplem4  22311  mp2pm2mplem5  22312  mp2pm2mp  22313  chpmat1d  22338  chpscmatgsummon  22347  chfacfpmmulgsum2  22367  xkocnv  23318  submtmd  23608  prdsdsf  23873  ressprdsds  23877  blfvalps  23889  prdsxmslem2  24038  tmsxpsval  24047  ngpds  24113  sgrimval  24141  subgngp  24144  tngngp  24171  tngngp3  24173  isnlm  24192  lssnlm  24218  isphtpy  24497  isphtpc  24510  pi1cpbl  24560  pi1addf  24563  pi1addval  24564  pi1grplem  24565  clmsub  24596  clmvsass  24605  clmvsdir  24607  isclmp  24613  cvsdiv  24648  iscph  24687  cphdir  24722  cphdi  24723  cph2di  24724  cph2subdi  24727  cphass  24728  tcphval  24735  ipcau2  24751  tcphcphlem1  24752  tcphcphlem2  24753  cphsscph  24768  caufval  24792  rrxip  24907  rrxvsca  24911  rrxplusgvscavalb  24912  rrxdsfival  24930  ehleudisval  24936  dvlip2  25512  q1pval  25671  r1pval  25674  dvntaylp  25883  efabl  26059  efsubm  26060  dchrmul  26751  istrkgc  27736  istrkgb  27737  istrkgcb  27738  istrkge  27739  istrkgl  27740  istrkgld  27741  iscgrg  27794  isismt  27816  tglngval  27833  legval  27866  ishlg  27884  mirval  27937  israg  27979  ishpg  28041  lmif  28067  islmib  28069  isinag  28120  ttgval  28157  ttgvalOLD  28158  wksonproplem  28992  wksonproplemOLD  28993  wspthsnon  29137  iswwlksnon  29138  iswspthsnon  29141  isconngr  29473  isconngr1  29474  grpodivval  29819  dipfval  29986  ipval  29987  sspgval  30013  sspsval  30015  lnoval  30036  ajfval  30093  dipdir  30126  dipass  30129  htth  30202  isomnd  32250  submomnd  32259  inftmrel  32357  isinftm  32358  isslmd  32378  isorng  32448  suborng  32464  resv1r  32487  lsmidllsp  32541  idlinsubrg  32580  prmidlval  32586  idlsrgval  32648  idlsrg0g  32651  rprmval  32664  asclply1subcl  32691  ply1chr  32692  drgextlsp  32712  fedgmullem1  32745  fedgmullem2  32746  fedgmul  32747  extdg1id  32773  smatlem  32808  submatminr1  32821  metidval  32901  pstmval  32906  pstmfval  32907  zlm0  32971  zlm1  32972  sitmval  33379  breprexp  33676  istrkg2d  33709  afsval  33714  mclsrcl  34583  mppsval  34594  bj-endval  36244  matunitlindflem2  36533  istotbnd  36685  isbnd  36696  rrnequiv  36751  isrngo  36813  rngohomval  36880  idlval  36929  pridlval  36949  lflset  37977  islfld  37980  ldualvadd  38047  ldualsmul  38053  ldualvs  38055  isopos  38098  cmtfvalN  38128  iscvlat  38241  ishlat1  38270  lineset  38657  psubspset  38663  paddfval  38716  paddval  38717  ltrnfset  39036  trnfsetN  39074  trlfset  39079  tgrpov  39667  erngplus  39722  erngmul  39725  erngplus-rN  39730  erngmul-rN  39733  erngdvlem3  39909  erngdvlem4  39910  erng0g  39913  erngdvlem3-rN  39917  erngdvlem4-rN  39918  dvaplusg  39928  dvamulr  39931  dvavadd  39934  dvavsca  39936  dvalveclem  39944  dvhmulr  40005  dvhfvadd  40010  dvhvadd  40011  dvhopvadd2  40013  dvhvaddcl  40014  dvhvaddcomN  40015  dvhvsca  40020  dvhlveclem  40027  dvh0g  40030  djavalN  40054  diblsmopel  40090  dicvaddcl  40109  cdlemn6  40121  dihffval  40149  dihopelvalcpre  40167  djhval  40317  lcdvaddval  40517  lcdsmul  40521  lcdvsval  40523  lcdlkreq2N  40542  hvmapffval  40677  hvmapfval  40678  hdmap1fval  40715  hgmapffval  40804  hgmapfval  40805  hgmapadd  40813  hlhilipval  40872  hlhilhillem  40883  selvvvval  41205  mhphf2  41218  prjspval  41393  prjspner1  41416  mnringvald  43015  ioorrnopnlem  45068  hoidmvval0b  45354  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvle  45364  ovnhoi  45367  hoiqssbl  45389  hspmbllem2  45391  vonioo  45446  vonicc  45449  ismgmd  46594  ismgmhm  46601  issubmgm  46607  resmgmhm  46616  resmgmhm2  46617  resmgmhm2b  46618  idfusubc  46688  rngpropd  46721  rnghmval  46737  subrngmcl  46784  rnglidlmmgm  46804  rnglidlmsgrp  46805  rnglidlrng  46806  rngqiprngghmlem3  46822  rngqiprngimfolem  46823  rngqiprnglinlem1  46824  rngqiprngimf1  46833  rngqiprnglin  46835  rng2idl1cntr  46838  rngqiprngfulem5  46848  zlidlring  46874  uzlidlring  46875  rnghmresel  46910  rngchom  46913  rngcco  46917  rnghmsubcsetclem1  46921  rhmresel  46956  ringchom  46959  ringcco  46963  rhmsubcsetclem1  46967  rhmsubcrngclem1  46973  irinitoringc  47015  ovmpordxf  47062  lincop  47137  lincval  47138  lincsum  47158  lincscm  47159  lmod1lem2  47217  lmod1lem3  47218  lmod1lem4  47219  ldepsnlinc  47237  lines  47465  line  47466  rrxlines  47467  rrxline  47468  spheres  47480  fvconstr  47570  fvconstrn0  47571  fvconstr2  47572  catprs  47679  thincmod  47699  isthincd2lem2  47704  isthincd  47705  mndtcco2  47760  mndtccatid  47761  grptcmon  47764  grptcepi  47765