Theorem oveqd 7437

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveq123d  7441  oveqdr  7448  csbov  7465  csbov12g  7466  ovmpodxf  7570  oprssov  7590  2mpo0  7670  ofeqd  7695  mptmpoopabbrd  8094  mptmpoopabovd  8095  el2mpocsbcl  8096  fnmpoovd  8098  frecseq123  8300  ruclem1  16399  vdwapval  17151  vdwapid1  17153  vdwmc2  17157  vdwpc  17158  vdwlem5  17163  vdwlem8  17166  vdwlem13  17171  prdsval  17626  prdsdsval2  17655  pwsplusgval  17662  pwsmulrval  17663  pwsvscafval  17666  imasval  17683  iscat  17846  iscatd  17847  catidex  17848  catideu  17849  cidfval  17850  cidval  17851  catidd  17854  iscatd2  17855  catlid  17857  catrid  17858  homffval  17864  homfeqd  17869  homfeqval  17871  comfffval  17872  comffval  17873  comfeq  17880  comfeqd  17881  comfeqval  17882  catpropd  17883  oppcval  17887  oppcco  17891  monfval  17907  ismon  17908  oppcmon  17913  oppcepi  17914  sectffval  17925  sectfval  17926  invffval  17933  isoval  17940  dfiso2  17947  isofn  17950  invisoinvl  17965  invcoisoid  17967  isocoinvid  17968  issubc  18010  issubc3  18024  isfunc  18039  cofuval  18057  cofuval2  18062  funcres  18071  funcres2b  18072  funcres2  18073  idfusubc  18075  funcres2c  18078  isfull  18087  isfth  18091  fullres2c  18116  natfval  18124  isnat  18125  fucval  18136  fucco  18140  fucpropd  18155  initoval  18168  termoval  18169  homarcl  18203  coafval  18239  resssetc  18267  resscatc  18284  catciso  18286  xpcval  18351  1stfval  18365  2ndfval  18368  prfval  18373  prfcl  18377  evlfval  18391  curfval  18397  curf1cl  18402  curfcl  18406  uncf1  18410  uncf2  18411  diag12  18418  diag2  18419  curf2ndf  18421  hofval  18426  hof1  18428  hof2fval  18429  hofcl  18433  yon12  18439  yon2  18440  hofpropd  18441  joinval  18549  meetval  18563  isdlat  18696  plusffval  18822  ismgmd  18830  issstrmgm  18831  grpidval  18840  grpidd  18852  idressid  18862  gsumvalx  18865  gsumpropd  18867  gsumress  18871  ismgmhm  18885  issubmgm  18891  resmgmhm  18900  resmgmhm2  18901  resmgmhm2b  18902  issgrpd  18919  ismndd  18946  issubmnd  18953  submnd0OLD  18957  ismhm  18980  issubm  18998  resmhm  19016  resmhm2  19017  resmhm2b  19018  mhmimalem  19020  isgrp  19150  isgrpd2e  19166  grpidd2  19188  grpinvfval  19189  grpinvfvalALT  19190  imasgrp2  19265  imasgrp  19266  subg0  19342  subginv  19343  subgcl  19346  issubgrpd2  19353  isnsg  19365  isghm  19430  resghm  19446  isga  19505  subgga  19514  gasubg  19516  cntzfval  19534  resscntz  19547  odfval  19746  odfvalALT  19747  gexval  19792  lsmfval  19852  lsmvalx  19853  oppglsm  19856  subglsm  19887  pj1fval  19908  efgtval  19937  iscmn  20003  iscmnd  20008  submcmn2  20053  imasabl  20090  iscyg  20093  cycsubmcmn  20103  isomnd  20337  submomnd  20346  prdsmgp  20371  rngpropd  20396  ringurd  20411  issrg  20414  isring  20463  ringidss  20506  mulgass3  20583  dvdsrval  20591  rdivmuldivd  20643  isirred  20649  rnghmval  20670  rhmval0  20705  islring  20792  lringuplu  20796  subrngmcl  20809  subrg1  20834  subrgdvds  20838  subrguss  20839  subrginv  20840  subrgdv  20841  subrgunit  20842  subrgugrp  20843  rnghmresel  20872  rngchom  20875  rngcco  20879  rnghmsubcsetclem1  20883  rhmresel  20901  ringchom  20904  ringcco  20908  rhmsubcsetclem1  20912  rhmsubcrngclem1  20918  rrgval  20949  isdrngd  21022  isdrngrd  21023  isdrngdOLD  21024  isdrngrdOLD  21025  abvfval  21067  isabvd  21069  issrngd  21112  isorng  21118  suborng  21133  islmod  21139  islmodd  21141  scaffval  21155  lmodpropd  21200  lssset  21208  islssd  21210  prdslmodd  21244  islmhm  21302  reslmhm  21327  reslmhm2  21328  reslmhm2b  21329  islbs  21351  rlmvneg  21481  rnglidlmmgm  21533  rnglidlmsgrp  21534  rnglidlrng  21535  lsmidllsp  21537  rngqiprngghmlem3  21585  rngqiprngimfolem  21586  rngqiprnglinlem1  21587  rngqiprngimf1  21596  rngqiprnglin  21598  rng2idl1cntr  21601  rngqiprngfulem5  21611  prmidlval  21618  irinitoringc  21785  isphl  21934  ipffval  21954  isphld  21960  phssipval  21963  phssip  21964  phlssphl  21965  ocvfval  21972  isobs  22026  frlmplusgval  22070  frlmsubgval  22071  frlmvscafval  22072  frlmip  22084  frlmipval  22085  frlmup1  22104  lsslindf  22136  isassa  22164  isassad  22173  sraassab  22176  assamulgscmlem2  22208  psrval  22223  resspsradd  22282  resspsrmul  22283  resspsrvsca  22284  mplmon2mul  22378  selvvvval  22451  ply1coe  22616  ply1chr  22624  lply1binomsc  22629  evl1expd  22663  evl1scvarpw  22681  asclply1subcl  22692  mamufval  22707  matplusg2  22742  matvsca2  22743  matplusgcell  22748  matsubgcell  22749  matinvgcell  22750  matvscacell  22751  matmulcell  22760  mpomatmul  22761  mat1  22762  mattposm  22774  mat1dimmul  22791  dmatmul  22812  dmatcrng  22817  scmataddcl  22831  scmatsubcl  22832  scmatcrng  22836  smatvscl  22839  scmatghm  22848  scmatmhm  22849  mvmulfval  22857  ma1repveval  22886  mdetrlin  22917  mdetrsca  22918  mdetmul  22938  madurid  22959  minmar1cl  22966  smadiadetglem1  22986  smadiadetr  22990  matinv  22992  matunitlindflem2  22995  slesolinv  22998  slesolinvbi  22999  cramerimplem3  23003  cpmatacl  23034  mat2pmatghm  23048  decpmatmullem  23089  decpmatmul  23090  pmatcollpw1lem1  23092  pmatcollpw2lem  23095  pmatcollpwlem  23098  pmatcollpw3lem  23101  mply1topmatval  23122  mp2pm2mplem1  23124  mp2pm2mplem4  23127  mp2pm2mplem5  23128  mp2pm2mp  23129  chpmat1d  23154  chpscmatgsummon  23163  chfacfpmmulgsum2  23183  xkocnv  24133  submtmd  24423  prdsdsf  24686  ressprdsds  24690  blfvalps  24702  prdsxmslem2  24848  tmsxpsval  24857  ngpds  24923  sgrimval  24951  subgngp  24954  tngngp  24973  tngngp3  24975  isnlm  24994  lssnlm  25020  isphtpy  25302  isphtpc  25315  pi1cpbl  25365  pi1addf  25368  pi1addval  25369  pi1grplem  25370  clmsub  25401  clmvsass  25410  clmvsdir  25412  isclmp  25418  cvsdiv  25453  iscph  25491  cphdir  25526  cphdi  25527  cph2di  25528  cph2subdi  25531  cphass  25532  tcphval  25539  ipcau2  25555  tcphcphlem1  25556  tcphcphlem2  25557  cphsscph  25572  caufval  25596  rrxip  25711  rrxvsca  25715  rrxplusgvscavalb  25716  rrxdsfival  25734  ehleudisval  25740  dvlip2  26315  q1pval  26473  r1pval  26476  dvntaylp  26698  efabl  26878  efsubm  26879  dchrmul  27575  seqseq123d  28672  istrkgc  28916  istrkgb  28917  istrkgcb  28918  istrkge  28919  istrkgl  28920  istrkgld  28921  iscgrg  28975  isismt  28997  tglngval  29014  legval  29047  ishlg2  29065  ishlg  29068  mirval  29127  israg  29172  ishpg  29237  tgplnfn  29253  plngval  29255  isplng  29256  lmif  29290  islmib  29292  isinag  29357  angmgmval  29394  ttgval  29452  wksonproplem  30287  wspthsnon  30441  iswwlksnon  30442  iswspthsnon  30445  isconngr  30790  isconngr1  30791  grpodivval  31137  dipfval  31304  ipval  31305  sspgval  31331  sspsval  31333  lnoval  31354  ajfval  31411  dipdir  31444  dipass  31447  htth  31520  ressmulgnn0d  33605  inftmrel  33741  isinftm  33742  isslmd  33763  elrgspnlem1  33803  erlval  33819  rlocval  33820  rlocaddval  33830  rlocmulval  33831  subrdom  33846  resv1r  33900  idlinsubrg  33981  idlsrgval  34035  idlsrg0g  34038  rprmval  34048  ressply1evls1  34097  vietalem  34211  drgextlsp  34226  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  extdg1id  34298  fldextrspunlsplem  34305  fldextrspunlsp  34306  extdgfialglem1  34324  extdgfialglem2  34325  algextdeglem8  34356  smatlem  34429  submatminr1  34442  metidval  34522  pstmval  34527  pstmfval  34528  zlm0  34592  zlm1  34593  sitmval  34981  breprexp  35262  istrkg2d  35295  afsval  35303  mclsrcl  36326  mppsval  36337  bj-endval  38237  istotbnd  38704  isbnd  38715  rrnequiv  38770  isrngo  38832  rngohomval  38899  idlval  38948  pridlval  38968  lflset  40117  islfld  40120  ldualvadd  40187  ldualsmul  40193  ldualvs  40195  isopos  40238  cmtfvalN  40268  iscvlat  40381  ishlat1  40410  lineset  40796  psubspset  40802  paddfval  40855  paddval  40856  ltrnfset  41175  trnfsetN  41213  trlfset  41218  tgrpov  41806  erngplus  41861  erngmul  41864  erngplus-rN  41869  erngmul-rN  41872  erngdvlem3  42048  erngdvlem4  42049  erng0g  42052  erngdvlem3-rN  42056  erngdvlem4-rN  42057  dvaplusg  42067  dvamulr  42070  dvavadd  42073  dvavsca  42075  dvalveclem  42083  dvhmulr  42144  dvhfvadd  42149  dvhvadd  42150  dvhopvadd2  42152  dvhvaddcl  42153  dvhvaddcomN  42154  dvhvsca  42159  dvhlveclem  42166  dvh0g  42169  djavalN  42193  diblsmopel  42229  dicvaddcl  42248  cdlemn6  42260  dihffval  42288  dihopelvalcpre  42306  djhval  42456  lcdvaddval  42656  lcdsmul  42660  lcdvsval  42662  lcdlkreq2N  42681  hvmapffval  42816  hvmapfval  42817  hdmap1fval  42854  hgmapffval  42943  hgmapfval  42944  hgmapadd  42952  hlhilipval  43007  hlhilhillem  43018  isprimroot  43144  aks6d1c1p4  43162  idomnnzpownz  43183  aks6d1c5lem1  43187  aks6d1c5lem3  43188  aks6d1c5lem2  43189  aks5lem3a  43240  unitscyglem5  43250  rhmpsr1  43613  mhphf2  43627  prjspval  43632  sn-isghm  43685  mnringvald  45211  ioorrnopnlem  47314  hoidmvval0b  47600  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvle  47610  ovnhoi  47613  hoiqssbl  47635  hspmbllem2  47637  vonioo  47692  vonicc  47695  zlidlring  49331  uzlidlring  49332  ovmpordxf  49451  lincop  49520  lincval  49521  lincsum  49541  lincscm  49542  lmod1lem2  49600  lmod1lem3  49601  lmod1lem4  49602  ldepsnlinc  49620  lines  49843  line  49844  rrxlines  49845  rrxline  49846  spheres  49858  ovconstbrd  49972  ovconstbrn0d  49973  elovconstbrd  49974  catprs  50119  sectrcl2  50131  invrcl2  50133  invfn  50138  isorcl2  50142  sectpropdlem  50144  invpropdlem  50146  isopropdlem  50148  cicpropdlem  50157  iinfconstbas  50174  nelsubclem  50175  nelsubc3lem  50178  ssccatid  50180  resccatlem  50181  cofu2a  50203  cofid2a  50221  cofid2  50223  cofidf2a  50225  cofidf2  50228  oppf2  50248  upfval  50284  upfval2  50285  upfval3  50286  upeu3  50303  upeu4  50304  oppcup3  50317  natoppfb  50339  swapfval  50370  swapf2a  50379  1stfpropd  50398  2ndfpropd  50399  cofuswapf2  50403  tposcurf12  50406  tposcurf2  50408  tposcurf2cl  50410  fucofvalg  50426  fuco11b  50445  fuco23a  50460  precofval3  50479  prcofpropd  50487  catcrcl2  50504  opf12  50512  fucoppcco  50517  thincmod  50538  isthincd2lem2  50543  isthincd  50544  dfinito4  50609  mndtcco2  50694  mndtccatid  50695  oppgoppchom  50698  oppgoppcco  50699  grptcmon  50701  grptcepi  50702  2arwcatlem2  50704  2arwcatlem3  50705  2arwcatlem4  50706  2arwcat  50708  lanrcl  50729  ranrcl  50730  rellan  50731  relran  50732  concom  50771  coccom  50772