Theorem oveqd 7465

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

Syntax hints:   → wi 4   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveq123d  7469  oveqdr  7476  csbov  7493  csbov12g  7494  ovmpodxf  7600  oprssov  7619  2mpo0  7699  ofeqd  7716  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabovd  8123  mptmpoopabbrdOLDOLD  8124  mptmpoopabovdOLD  8125  el2mpocsbcl  8126  fnmpoovd  8128  frecseq123  8323  ruclem1  16279  vdwapval  17020  vdwapid1  17022  vdwmc2  17026  vdwpc  17027  vdwlem5  17032  vdwlem8  17035  vdwlem13  17040  prdsval  17515  prdsdsval2  17544  pwsplusgval  17550  pwsmulrval  17551  pwsvscafval  17554  imasval  17571  iscat  17730  iscatd  17731  catidex  17732  catideu  17733  cidfval  17734  cidval  17735  catidd  17738  iscatd2  17739  catlid  17741  catrid  17742  homffval  17748  homfeqd  17753  homfeqval  17755  comfffval  17756  comffval  17757  comfeq  17764  comfeqd  17765  comfeqval  17766  catpropd  17767  oppcval  17771  oppcco  17776  monfval  17793  ismon  17794  oppcmon  17799  oppcepi  17800  sectffval  17811  sectfval  17812  invffval  17819  isoval  17826  dfiso2  17833  isofn  17836  invisoinvl  17851  invcoisoid  17853  isocoinvid  17854  issubc  17899  issubc3  17913  isfunc  17928  cofuval  17946  cofuval2  17951  funcres  17960  funcres2b  17961  funcres2  17962  idfusubc  17964  funcres2c  17968  isfull  17977  isfth  17981  fullres2c  18006  natfval  18014  isnat  18015  fucval  18027  fucco  18032  fucpropd  18047  initoval  18060  termoval  18061  homarcl  18095  coafval  18131  resssetc  18159  resscatc  18176  catciso  18178  xpcval  18246  1stfval  18260  2ndfval  18263  prfval  18268  prfcl  18272  evlfval  18287  curfval  18293  curf1cl  18298  curfcl  18302  uncf1  18306  uncf2  18307  diag12  18314  diag2  18315  curf2ndf  18317  hofval  18322  hof1  18324  hof2fval  18325  hofcl  18329  yon12  18335  yon2  18336  hofpropd  18337  joinval  18447  meetval  18461  isdlat  18592  plusffval  18684  ismgmd  18690  issstrmgm  18691  grpidval  18699  grpidd  18709  gsumvalx  18714  gsumpropd  18716  gsumress  18720  ismgmhm  18734  issubmgm  18740  resmgmhm  18749  resmgmhm2  18750  resmgmhm2b  18751  issgrpd  18768  ismndd  18794  issubmnd  18799  submnd0  18801  ismhm  18820  issubm  18838  resmhm  18855  resmhm2  18856  resmhm2b  18857  mhmimalem  18859  isgrp  18979  isgrpd2e  18995  grpidd2  19017  grpinvfval  19018  grpinvfvalALT  19019  imasgrp2  19095  imasgrp  19096  subg0  19172  subginv  19173  subgcl  19176  issubgrpd2  19182  isnsg  19195  isghm  19255  isghmOLD  19256  resghm  19272  isga  19331  subgga  19340  gasubg  19342  cntzfval  19360  resscntz  19373  odfval  19574  odfvalALT  19575  gexval  19620  lsmfval  19680  lsmvalx  19681  oppglsm  19684  subglsm  19715  pj1fval  19736  efgtval  19765  iscmn  19831  iscmnd  19836  submcmn2  19881  imasabl  19918  iscyg  19921  cycsubmcmn  19931  prdsmgp  20178  rngpropd  20201  ringurd  20212  issrg  20215  isring  20264  ringidss  20300  mulgass3  20379  dvdsrval  20387  rdivmuldivd  20439  isirred  20445  rnghmval  20466  islring  20566  lringuplu  20570  subrngmcl  20583  subrg1  20610  subrgdvds  20614  subrguss  20615  subrginv  20616  subrgdv  20617  subrgunit  20618  subrgugrp  20619  rnghmresel  20642  rngchom  20645  rngcco  20649  rnghmsubcsetclem1  20653  rhmresel  20671  ringchom  20674  ringcco  20678  rhmsubcsetclem1  20682  rhmsubcrngclem1  20688  rrgval  20719  isdrngd  20787  isdrngrd  20788  isdrngdOLD  20789  isdrngrdOLD  20790  abvfval  20833  isabvd  20835  issrngd  20878  islmod  20884  islmodd  20886  scaffval  20900  lmodpropd  20945  lssset  20954  islssd  20956  prdslmodd  20990  islmhm  21049  reslmhm  21074  reslmhm2  21075  reslmhm2b  21076  islbs  21098  rlmvneg  21236  rnglidlmmgm  21278  rnglidlmsgrp  21279  rnglidlrng  21280  rngqiprngghmlem3  21322  rngqiprngimfolem  21323  rngqiprnglinlem1  21324  rngqiprngimf1  21333  rngqiprnglin  21335  rng2idl1cntr  21338  rngqiprngfulem5  21348  irinitoringc  21513  isphl  21669  ipffval  21689  isphld  21695  phssipval  21698  phssip  21699  phlssphl  21700  ocvfval  21707  isobs  21763  frlmplusgval  21807  frlmsubgval  21808  frlmvscafval  21809  frlmip  21821  frlmipval  21822  frlmup1  21841  lsslindf  21873  isassa  21899  isassad  21908  sraassab  21911  assamulgscmlem2  21943  psrval  21958  resspsradd  22018  resspsrmul  22019  resspsrvsca  22020  mplmon2mul  22116  ply1coe  22323  ply1chr  22331  lply1binomsc  22336  evl1expd  22370  evl1scvarpw  22388  asclply1subcl  22399  mamufval  22417  matplusg2  22454  matvsca2  22455  matplusgcell  22460  matsubgcell  22461  matinvgcell  22462  matvscacell  22463  matmulcell  22472  mpomatmul  22473  mat1  22474  mattposm  22486  mat1dimmul  22503  dmatmul  22524  dmatcrng  22529  scmataddcl  22543  scmatsubcl  22544  scmatcrng  22548  smatvscl  22551  scmatghm  22560  scmatmhm  22561  mvmulfval  22569  ma1repveval  22598  mdetrlin  22629  mdetrsca  22630  mdetmul  22650  madurid  22671  minmar1cl  22678  smadiadetglem1  22698  smadiadetr  22702  matinv  22704  slesolinv  22707  slesolinvbi  22708  cramerimplem3  22712  cpmatacl  22743  mat2pmatghm  22757  decpmatmullem  22798  decpmatmul  22799  pmatcollpw1lem1  22801  pmatcollpw2lem  22804  pmatcollpwlem  22807  pmatcollpw3lem  22810  mply1topmatval  22831  mp2pm2mplem1  22833  mp2pm2mplem4  22836  mp2pm2mplem5  22837  mp2pm2mp  22838  chpmat1d  22863  chpscmatgsummon  22872  chfacfpmmulgsum2  22892  xkocnv  23843  submtmd  24133  prdsdsf  24398  ressprdsds  24402  blfvalps  24414  prdsxmslem2  24563  tmsxpsval  24572  ngpds  24638  sgrimval  24666  subgngp  24669  tngngp  24696  tngngp3  24698  isnlm  24717  lssnlm  24743  isphtpy  25032  isphtpc  25045  pi1cpbl  25096  pi1addf  25099  pi1addval  25100  pi1grplem  25101  clmsub  25132  clmvsass  25141  clmvsdir  25143  isclmp  25149  cvsdiv  25184  iscph  25223  cphdir  25258  cphdi  25259  cph2di  25260  cph2subdi  25263  cphass  25264  tcphval  25271  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  cphsscph  25304  caufval  25328  rrxip  25443  rrxvsca  25447  rrxplusgvscavalb  25448  rrxdsfival  25466  ehleudisval  25472  dvlip2  26054  q1pval  26214  r1pval  26217  dvntaylp  26431  efabl  26610  efsubm  26611  dchrmul  27310  seqseq123d  28310  istrkgc  28480  istrkgb  28481  istrkgcb  28482  istrkge  28483  istrkgl  28484  istrkgld  28485  iscgrg  28538  isismt  28560  tglngval  28577  legval  28610  ishlg  28628  mirval  28681  israg  28723  ishpg  28785  lmif  28811  islmib  28813  isinag  28864  ttgval  28901  ttgvalOLD  28902  wksonproplem  29740  wksonproplemOLD  29741  wspthsnon  29885  iswwlksnon  29886  iswspthsnon  29889  isconngr  30221  isconngr1  30222  grpodivval  30567  dipfval  30734  ipval  30735  sspgval  30761  sspsval  30763  lnoval  30784  ajfval  30841  dipdir  30874  dipass  30877  htth  30950  isomnd  33051  submomnd  33060  inftmrel  33160  isinftm  33161  isslmd  33181  erlval  33230  rlocval  33231  rlocaddval  33240  rlocmulval  33241  subrdom  33254  isorng  33294  suborng  33310  resv1r  33333  lsmidllsp  33393  idlinsubrg  33424  prmidlval  33430  idlsrgval  33496  idlsrg0g  33499  rprmval  33509  drgextlsp  33608  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33676  algextdeglem8  33715  smatlem  33743  submatminr1  33756  metidval  33836  pstmval  33841  pstmfval  33842  zlm0  33906  zlm1  33907  sitmval  34314  breprexp  34610  istrkg2d  34643  afsval  34648  mclsrcl  35529  mppsval  35540  bj-endval  37281  matunitlindflem2  37577  istotbnd  37729  isbnd  37740  rrnequiv  37795  isrngo  37857  rngohomval  37924  idlval  37973  pridlval  37993  lflset  39015  islfld  39018  ldualvadd  39085  ldualsmul  39091  ldualvs  39093  isopos  39136  cmtfvalN  39166  iscvlat  39279  ishlat1  39308  lineset  39695  psubspset  39701  paddfval  39754  paddval  39755  ltrnfset  40074  trnfsetN  40112  trlfset  40117  tgrpov  40705  erngplus  40760  erngmul  40763  erngplus-rN  40768  erngmul-rN  40771  erngdvlem3  40947  erngdvlem4  40948  erng0g  40951  erngdvlem3-rN  40955  erngdvlem4-rN  40956  dvaplusg  40966  dvamulr  40969  dvavadd  40972  dvavsca  40974  dvalveclem  40982  dvhmulr  41043  dvhfvadd  41048  dvhvadd  41049  dvhopvadd2  41051  dvhvaddcl  41052  dvhvaddcomN  41053  dvhvsca  41058  dvhlveclem  41065  dvh0g  41068  djavalN  41092  diblsmopel  41128  dicvaddcl  41147  cdlemn6  41159  dihffval  41187  dihopelvalcpre  41205  djhval  41355  lcdvaddval  41555  lcdsmul  41559  lcdvsval  41561  lcdlkreq2N  41580  hvmapffval  41715  hvmapfval  41716  hdmap1fval  41753  hgmapffval  41842  hgmapfval  41843  hgmapadd  41851  hlhilipval  41910  hlhilhillem  41921  isprimroot  42050  aks6d1c1p4  42068  idomnnzpownz  42089  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks5lem3a  42146  unitscyglem5  42156  rhmpsr1  42508  selvvvval  42540  mhphf2  42553  prjspval  42558  prjspner1  42581  sn-isghm  42628  mnringvald  44177  ioorrnopnlem  46225  hoidmvval0b  46511  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvle  46521  ovnhoi  46524  hoiqssbl  46546  hspmbllem2  46548  vonioo  46603  vonicc  46606  zlidlring  47957  uzlidlring  47958  ovmpordxf  48063  lincop  48137  lincval  48138  lincsum  48158  lincscm  48159  lmod1lem2  48217  lmod1lem3  48218  lmod1lem4  48219  ldepsnlinc  48237  lines  48465  line  48466  rrxlines  48467  rrxline  48468  spheres  48480  fvconstr  48569  fvconstrn0  48570  fvconstr2  48571  catprs  48678  thincmod  48698  isthincd2lem2  48703  isthincd  48704  mndtcco2  48759  mndtccatid  48760  grptcmon  48763  grptcepi  48764