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  27705  istrkgb  27706  istrkgcb  27707  istrkge  27708  istrkgl  27709  istrkgld  27710  iscgrg  27763  isismt  27785  tglngval  27802  legval  27835  ishlg  27853  mirval  27906  israg  27948  ishpg  28010  lmif  28036  islmib  28038  isinag  28089  ttgval  28126  ttgvalOLD  28127  wksonproplem  28961  wksonproplemOLD  28962  wspthsnon  29106  iswwlksnon  29107  iswspthsnon  29110  isconngr  29442  isconngr1  29443  grpodivval  29788  dipfval  29955  ipval  29956  sspgval  29982  sspsval  29984  lnoval  30005  ajfval  30062  dipdir  30095  dipass  30098  htth  30171  isomnd  32219  submomnd  32228  inftmrel  32326  isinftm  32327  isslmd  32347  isorng  32417  suborng  32433  resv1r  32456  lsmidllsp  32510  idlinsubrg  32549  prmidlval  32555  idlsrgval  32617  idlsrg0g  32620  rprmval  32633  asclply1subcl  32660  ply1chr  32661  drgextlsp  32681  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  extdg1id  32742  smatlem  32777  submatminr1  32790  metidval  32870  pstmval  32875  pstmfval  32876  zlm0  32940  zlm1  32941  sitmval  33348  breprexp  33645  istrkg2d  33678  afsval  33683  mclsrcl  34552  mppsval  34563  bj-endval  36196  matunitlindflem2  36485  istotbnd  36637  isbnd  36648  rrnequiv  36703  isrngo  36765  rngohomval  36832  idlval  36881  pridlval  36901  lflset  37929  islfld  37932  ldualvadd  37999  ldualsmul  38005  ldualvs  38007  isopos  38050  cmtfvalN  38080  iscvlat  38193  ishlat1  38222  lineset  38609  psubspset  38615  paddfval  38668  paddval  38669  ltrnfset  38988  trnfsetN  39026  trlfset  39031  tgrpov  39619  erngplus  39674  erngmul  39677  erngplus-rN  39682  erngmul-rN  39685  erngdvlem3  39861  erngdvlem4  39862  erng0g  39865  erngdvlem3-rN  39869  erngdvlem4-rN  39870  dvaplusg  39880  dvamulr  39883  dvavadd  39886  dvavsca  39888  dvalveclem  39896  dvhmulr  39957  dvhfvadd  39962  dvhvadd  39963  dvhopvadd2  39965  dvhvaddcl  39966  dvhvaddcomN  39967  dvhvsca  39972  dvhlveclem  39979  dvh0g  39982  djavalN  40006  diblsmopel  40042  dicvaddcl  40061  cdlemn6  40073  dihffval  40101  dihopelvalcpre  40119  djhval  40269  lcdvaddval  40469  lcdsmul  40473  lcdvsval  40475  lcdlkreq2N  40494  hvmapffval  40629  hvmapfval  40630  hdmap1fval  40667  hgmapffval  40756  hgmapfval  40757  hgmapadd  40765  hlhilipval  40824  hlhilhillem  40835  selvvvval  41157  mhphf2  41170  prjspval  41345  prjspner1  41368  mnringvald  42967  ioorrnopnlem  45020  hoidmvval0b  45306  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvle  45316  ovnhoi  45319  hoiqssbl  45341  hspmbllem2  45343  vonioo  45398  vonicc  45401  ismgmd  46546  ismgmhm  46553  issubmgm  46559  resmgmhm  46568  resmgmhm2  46569  resmgmhm2b  46570  idfusubc  46640  rngpropd  46673  rnghmval  46689  subrngmcl  46736  rnglidlmmgm  46756  rnglidlmsgrp  46757  rnglidlrng  46758  rngqiprngghmlem3  46774  rngqiprngimfolem  46775  rngqiprnglinlem1  46776  rngqiprngimf1  46785  rngqiprnglin  46787  rng2idl1cntr  46790  rngqiprngfulem5  46800  zlidlring  46826  uzlidlring  46827  rnghmresel  46862  rngchom  46865  rngcco  46869  rnghmsubcsetclem1  46873  rhmresel  46908  ringchom  46911  ringcco  46915  rhmsubcsetclem1  46919  rhmsubcrngclem1  46925  irinitoringc  46967  ovmpordxf  47014  lincop  47089  lincval  47090  lincsum  47110  lincscm  47111  lmod1lem2  47169  lmod1lem3  47170  lmod1lem4  47171  ldepsnlinc  47189  lines  47417  line  47418  rrxlines  47419  rrxline  47420  spheres  47432  fvconstr  47522  fvconstrn0  47523  fvconstr2  47524  catprs  47631  thincmod  47651  isthincd2lem2  47656  isthincd  47657  mndtcco2  47712  mndtccatid  47713  grptcmon  47716  grptcepi  47717