Theorem oveqd 7440

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  oveq123d  7444  oveqdr  7451  csbov  7468  csbov12g  7469  ovmpodxf  7573  oprssov  7592  2mpo0  7672  ofeqd  7689  mptmpoopabbrd  8087  mptmpoopabovd  8088  el2mpocsbcl  8089  fnmpoovd  8091  frecseq123  8288  ruclem1  16312  vdwapval  17058  vdwapid1  17060  vdwmc2  17064  vdwpc  17065  vdwlem5  17070  vdwlem8  17073  vdwlem13  17078  prdsval  17533  prdsdsval2  17562  pwsplusgval  17569  pwsmulrval  17570  pwsvscafval  17573  imasval  17590  iscat  17753  iscatd  17754  catidex  17755  catideu  17756  cidfval  17757  cidval  17758  catidd  17761  iscatd2  17762  catlid  17764  catrid  17765  homffval  17771  homfeqd  17776  homfeqval  17778  comfffval  17779  comffval  17780  comfeq  17787  comfeqd  17788  comfeqval  17789  catpropd  17790  oppcval  17794  oppcco  17798  monfval  17814  ismon  17815  oppcmon  17820  oppcepi  17821  sectffval  17832  sectfval  17833  invffval  17840  isoval  17847  dfiso2  17854  isofn  17857  invisoinvl  17872  invcoisoid  17874  isocoinvid  17875  issubc  17917  issubc3  17931  isfunc  17946  cofuval  17964  cofuval2  17969  funcres  17978  funcres2b  17979  funcres2  17980  idfusubc  17982  funcres2c  17985  isfull  17994  isfth  17998  fullres2c  18023  natfval  18031  isnat  18032  fucval  18043  fucco  18047  fucpropd  18062  initoval  18075  termoval  18076  homarcl  18110  coafval  18146  resssetc  18174  resscatc  18191  catciso  18193  xpcval  18258  1stfval  18272  2ndfval  18275  prfval  18280  prfcl  18284  evlfval  18298  curfval  18304  curf1cl  18309  curfcl  18313  uncf1  18317  uncf2  18318  diag12  18325  diag2  18326  curf2ndf  18328  hofval  18333  hof1  18335  hof2fval  18336  hofcl  18340  yon12  18346  yon2  18347  hofpropd  18348  joinval  18456  meetval  18470  isdlat  18603  plusffval  18729  ismgmd  18735  issstrmgm  18736  grpidval  18744  grpidd  18755  idressid  18762  gsumvalx  18763  gsumpropd  18765  gsumress  18769  ismgmhm  18783  issubmgm  18789  resmgmhm  18798  resmgmhm2  18799  resmgmhm2b  18800  issgrpd  18817  ismndd  18843  issubmnd  18848  submnd0OLD  18852  ismhm  18874  issubm  18892  resmhm  18910  resmhm2  18911  resmhm2b  18912  mhmimalem  18914  isgrp  19037  isgrpd2e  19053  grpidd2  19075  grpinvfval  19076  grpinvfvalALT  19077  imasgrp2  19152  imasgrp  19153  subg0  19229  subginv  19230  subgcl  19233  issubgrpd2  19240  isnsg  19252  isghm  19317  resghm  19333  isga  19392  subgga  19401  gasubg  19403  cntzfval  19421  resscntz  19434  odfval  19633  odfvalALT  19634  gexval  19679  lsmfval  19739  lsmvalx  19740  oppglsm  19743  subglsm  19774  pj1fval  19795  efgtval  19824  iscmn  19890  iscmnd  19895  submcmn2  19940  imasabl  19977  iscyg  19980  cycsubmcmn  19990  isomnd  20224  submomnd  20233  prdsmgp  20258  rngpropd  20283  ringurd  20298  issrg  20301  isring  20350  ringidss  20392  mulgass3  20468  dvdsrval  20476  rdivmuldivd  20528  isirred  20534  rnghmval  20555  rhmval0  20590  islring  20676  lringuplu  20680  subrngmcl  20693  subrg1  20718  subrgdvds  20722  subrguss  20723  subrginv  20724  subrgdv  20725  subrgunit  20726  subrgugrp  20727  rnghmresel  20756  rngchom  20759  rngcco  20763  rnghmsubcsetclem1  20767  rhmresel  20785  ringchom  20788  ringcco  20792  rhmsubcsetclem1  20796  rhmsubcrngclem1  20802  rrgval  20833  isdrngd  20905  isdrngrd  20906  isdrngdOLD  20907  isdrngrdOLD  20908  abvfval  20950  isabvd  20952  issrngd  20995  isorng  21001  suborng  21016  islmod  21022  islmodd  21024  scaffval  21038  lmodpropd  21083  lssset  21091  islssd  21093  prdslmodd  21127  islmhm  21185  reslmhm  21210  reslmhm2  21211  reslmhm2b  21212  islbs  21234  rlmvneg  21364  rnglidlmmgm  21416  rnglidlmsgrp  21417  rnglidlrng  21418  lsmidllsp  21420  rngqiprngghmlem3  21466  rngqiprngimfolem  21467  rngqiprnglinlem1  21468  rngqiprngimf1  21477  rngqiprnglin  21479  rng2idl1cntr  21482  rngqiprngfulem5  21492  prmidlval  21499  irinitoringc  21666  isphl  21815  ipffval  21835  isphld  21841  phssipval  21844  phssip  21845  phlssphl  21846  ocvfval  21853  isobs  21907  frlmplusgval  21951  frlmsubgval  21952  frlmvscafval  21953  frlmip  21965  frlmipval  21966  frlmup1  21985  lsslindf  22017  isassa  22043  isassad  22052  sraassab  22055  assamulgscmlem2  22087  psrval  22102  resspsradd  22161  resspsrmul  22162  resspsrvsca  22163  mplmon2mul  22257  selvvvval  22330  ply1coe  22495  ply1chr  22503  lply1binomsc  22508  evl1expd  22542  evl1scvarpw  22560  asclply1subcl  22571  mamufval  22586  matplusg2  22621  matvsca2  22622  matplusgcell  22627  matsubgcell  22628  matinvgcell  22629  matvscacell  22630  matmulcell  22639  mpomatmul  22640  mat1  22641  mattposm  22653  mat1dimmul  22670  dmatmul  22691  dmatcrng  22696  scmataddcl  22710  scmatsubcl  22711  scmatcrng  22715  smatvscl  22718  scmatghm  22727  scmatmhm  22728  mvmulfval  22736  ma1repveval  22765  mdetrlin  22796  mdetrsca  22797  mdetmul  22817  madurid  22838  minmar1cl  22845  smadiadetglem1  22865  smadiadetr  22869  matinv  22871  slesolinv  22874  slesolinvbi  22875  cramerimplem3  22879  cpmatacl  22910  mat2pmatghm  22924  decpmatmullem  22965  decpmatmul  22966  pmatcollpw1lem1  22968  pmatcollpw2lem  22971  pmatcollpwlem  22974  pmatcollpw3lem  22977  mply1topmatval  22998  mp2pm2mplem1  23000  mp2pm2mplem4  23003  mp2pm2mplem5  23004  mp2pm2mp  23005  chpmat1d  23030  chpscmatgsummon  23039  chfacfpmmulgsum2  23059  xkocnv  24008  submtmd  24298  prdsdsf  24561  ressprdsds  24565  blfvalps  24577  prdsxmslem2  24723  tmsxpsval  24732  ngpds  24798  sgrimval  24826  subgngp  24829  tngngp  24848  tngngp3  24850  isnlm  24869  lssnlm  24895  isphtpy  25177  isphtpc  25190  pi1cpbl  25240  pi1addf  25243  pi1addval  25244  pi1grplem  25245  clmsub  25276  clmvsass  25285  clmvsdir  25287  isclmp  25293  cvsdiv  25328  iscph  25366  cphdir  25401  cphdi  25402  cph2di  25403  cph2subdi  25406  cphass  25407  tcphval  25414  ipcau2  25430  tcphcphlem1  25431  tcphcphlem2  25432  cphsscph  25447  caufval  25471  rrxip  25586  rrxvsca  25590  rrxplusgvscavalb  25591  rrxdsfival  25609  ehleudisval  25615  dvlip2  26191  q1pval  26349  r1pval  26352  dvntaylp  26571  efabl  26752  efsubm  26753  dchrmul  27449  seqseq123d  28516  istrkgc  28760  istrkgb  28761  istrkgcb  28762  istrkge  28763  istrkgl  28764  istrkgld  28765  iscgrg  28818  isismt  28840  tglngval  28857  legval  28890  ishlg2  28908  ishlg  28911  mirval  28969  israg  29014  ishpg  29078  tgplnfn  29094  plngval  29096  isplng  29097  lmif  29131  islmib  29133  isinag  29192  ttgval  29261  wksonproplem  30089  wspthsnon  30238  iswwlksnon  30239  iswspthsnon  30242  isconngr  30577  isconngr1  30578  grpodivval  30924  dipfval  31091  ipval  31092  sspgval  31118  sspsval  31120  lnoval  31141  ajfval  31198  dipdir  31231  dipass  31234  htth  31307  ressmulgnn0d  33395  inftmrel  33531  isinftm  33532  isslmd  33553  elrgspnlem1  33593  erlval  33609  rlocval  33610  rlocaddval  33620  rlocmulval  33621  subrdom  33636  resv1r  33690  idlinsubrg  33770  idlsrgval  33824  idlsrg0g  33827  rprmval  33837  ressply1evls1  33886  vietalem  34000  drgextlsp  34015  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  extdg1id  34087  fldextrspunlsplem  34094  fldextrspunlsp  34095  extdgfialglem1  34113  extdgfialglem2  34114  algextdeglem8  34145  smatlem  34218  submatminr1  34231  metidval  34311  pstmval  34316  pstmfval  34317  zlm0  34381  zlm1  34382  sitmval  34770  breprexp  35051  istrkg2d  35084  afsval  35092  mclsrcl  36073  mppsval  36084  bj-endval  37999  matunitlindflem2  38308  istotbnd  38460  isbnd  38471  rrnequiv  38526  isrngo  38588  rngohomval  38655  idlval  38704  pridlval  38724  lflset  39873  islfld  39876  ldualvadd  39943  ldualsmul  39949  ldualvs  39951  isopos  39994  cmtfvalN  40024  iscvlat  40137  ishlat1  40166  lineset  40552  psubspset  40558  paddfval  40611  paddval  40612  ltrnfset  40931  trnfsetN  40969  trlfset  40974  tgrpov  41562  erngplus  41617  erngmul  41620  erngplus-rN  41625  erngmul-rN  41628  erngdvlem3  41804  erngdvlem4  41805  erng0g  41808  erngdvlem3-rN  41812  erngdvlem4-rN  41813  dvaplusg  41823  dvamulr  41826  dvavadd  41829  dvavsca  41831  dvalveclem  41839  dvhmulr  41900  dvhfvadd  41905  dvhvadd  41906  dvhopvadd2  41908  dvhvaddcl  41909  dvhvaddcomN  41910  dvhvsca  41915  dvhlveclem  41922  dvh0g  41925  djavalN  41949  diblsmopel  41985  dicvaddcl  42004  cdlemn6  42016  dihffval  42044  dihopelvalcpre  42062  djhval  42212  lcdvaddval  42412  lcdsmul  42416  lcdvsval  42418  lcdlkreq2N  42437  hvmapffval  42572  hvmapfval  42573  hdmap1fval  42610  hgmapffval  42699  hgmapfval  42700  hgmapadd  42708  hlhilipval  42763  hlhilhillem  42774  isprimroot  42900  aks6d1c1p4  42918  idomnnzpownz  42939  aks6d1c5lem1  42943  aks6d1c5lem3  42944  aks6d1c5lem2  42945  aks5lem3a  42996  unitscyglem5  43006  rhmpsr1  43356  mhphf2  43370  prjspval  43375  prjspner1  43398  sn-isghm  43445  mnringvald  44977  ioorrnopnlem  47058  hoidmvval0b  47344  hoidmvlelem2  47350  hoidmvlelem3  47351  hoidmvle  47354  ovnhoi  47357  hoiqssbl  47379  hspmbllem2  47381  vonioo  47436  vonicc  47439  zlidlring  49039  uzlidlring  49040  ovmpordxf  49159  lincop  49228  lincval  49229  lincsum  49249  lincscm  49250  lmod1lem2  49308  lmod1lem3  49309  lmod1lem4  49310  ldepsnlinc  49328  lines  49551  line  49552  rrxlines  49553  rrxline  49554  spheres  49566  fvconstr  49680  fvconstrn0  49681  fvconstr2  49682  catprs  49829  sectrcl2  49841  invrcl2  49843  invfn  49848  isorcl2  49852  sectpropdlem  49854  invpropdlem  49856  isopropdlem  49858  cicpropdlem  49867  iinfconstbas  49884  nelsubclem  49885  nelsubc3lem  49888  ssccatid  49890  resccatlem  49891  cofu2a  49913  cofid2a  49931  cofid2  49933  cofidf2a  49935  cofidf2  49938  oppf2  49958  upfval  49994  upfval2  49995  upfval3  49996  upeu3  50013  upeu4  50014  oppcup3  50027  natoppfb  50049  swapfval  50080  swapf2a  50089  1stfpropd  50108  2ndfpropd  50109  cofuswapf2  50113  tposcurf12  50116  tposcurf2  50118  tposcurf2cl  50120  fucofvalg  50136  fuco11b  50155  fuco23a  50170  precofval3  50189  prcofpropd  50197  catcrcl2  50214  opf12  50222  fucoppcco  50227  thincmod  50248  isthincd2lem2  50253  isthincd  50254  dfinito4  50319  mndtcco2  50404  mndtccatid  50405  oppgoppchom  50408  oppgoppcco  50409  grptcmon  50411  grptcepi  50412  2arwcatlem2  50414  2arwcatlem3  50415  2arwcatlem4  50416  2arwcat  50418  lanrcl  50439  ranrcl  50440  rellan  50441  relran  50442  concom  50481  coccom  50482