Theorem oveqd 7457

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  oveq123d  7461  oveqdr  7468  csbov  7485  csbov12g  7486  ovmpodxf  7591  oprssov  7611  2mpo0  7691  ofeqd  7716  mptmpoopabbrd  8116  mptmpoopabovd  8117  el2mpocsbcl  8118  fnmpoovd  8120  frecseq123  8325  ruclem1  16425  vdwapval  17177  vdwapid1  17179  vdwmc2  17183  vdwpc  17184  vdwlem5  17189  vdwlem8  17192  vdwlem13  17197  prdsval  17652  prdsdsval2  17681  pwsplusgval  17688  pwsmulrval  17689  pwsvscafval  17692  imasval  17709  iscat  17872  iscatd  17873  catidex  17874  catideu  17875  cidfval  17876  cidval  17877  catidd  17880  iscatd2  17881  catlid  17883  catrid  17884  homffval  17890  homfeqd  17895  homfeqval  17897  comfffval  17898  comffval  17899  comfeq  17906  comfeqd  17907  comfeqval  17908  catpropd  17909  oppcval  17913  oppcco  17917  monfval  17933  ismon  17934  oppcmon  17939  oppcepi  17940  sectffval  17951  sectfval  17952  invffval  17959  isoval  17966  dfiso2  17973  isofn  17976  invisoinvl  17991  invcoisoid  17993  isocoinvid  17994  issubc  18036  issubc3  18050  isfunc  18065  cofuval  18083  cofuval2  18088  funcres  18097  funcres2b  18098  funcres2  18099  idfusubc  18101  funcres2c  18104  isfull  18113  isfth  18117  fullres2c  18142  natfval  18150  isnat  18151  fucval  18162  fucco  18166  fucpropd  18181  initoval  18194  termoval  18195  homarcl  18229  coafval  18265  resssetc  18293  resscatc  18310  catciso  18312  xpcval  18377  1stfval  18391  2ndfval  18394  prfval  18399  prfcl  18403  evlfval  18417  curfval  18423  curf1cl  18428  curfcl  18432  uncf1  18436  uncf2  18437  diag12  18444  diag2  18445  curf2ndf  18447  hofval  18452  hof1  18454  hof2fval  18455  hofcl  18459  yon12  18465  yon2  18466  hofpropd  18467  joinval  18575  meetval  18589  isdlat  18722  plusffval  18848  ismgmd  18856  issstrmgm  18857  grpidval  18866  grpidd  18878  idressid  18888  gsumvalx  18891  gsumpropd  18893  gsumress  18897  ismgmhm  18911  issubmgm  18917  resmgmhm  18926  resmgmhm2  18927  resmgmhm2b  18928  issgrpd  18945  ismndd  18972  issubmnd  18979  submnd0OLD  18983  ismhm  19006  issubm  19024  resmhm  19042  resmhm2  19043  resmhm2b  19044  mhmimalem  19046  isgrp  19176  isgrpd2e  19192  grpidd2  19214  grpinvfval  19215  grpinvfvalALT  19216  imasgrp2  19291  imasgrp  19292  subg0  19368  subginv  19369  subgcl  19372  issubgrpd2  19379  isnsg  19391  isghm  19456  resghm  19472  isga  19532  subgga  19541  gasubg  19543  cntzfval  19561  resscntz  19574  odfval  19773  odfvalALT  19774  gexval  19819  lsmfval  19879  lsmvalx  19880  oppglsm  19883  subglsm  19914  pj1fval  19935  efgtval  19964  iscmn  20030  iscmnd  20035  submcmn2  20080  imasabl  20117  iscyg  20120  cycsubmcmn  20130  isomnd  20364  submomnd  20373  prdsmgp  20398  rngpropd  20423  ringurd  20438  issrg  20441  isring  20490  ringidss  20533  mulgass3  20610  dvdsrval  20618  rdivmuldivd  20670  isirred  20676  rnghmval  20697  rhmval0  20732  islring  20819  lringuplu  20823  subrngmcl  20836  subrg1  20861  subrgdvds  20865  subrguss  20866  subrginv  20867  subrgdv  20868  subrgunit  20869  subrgugrp  20870  rnghmresel  20899  rngchom  20902  rngcco  20906  rnghmsubcsetclem1  20910  rhmresel  20928  ringchom  20931  ringcco  20935  rhmsubcsetclem1  20939  rhmsubcrngclem1  20945  rrgval  20976  isdrngd  21049  isdrngrd  21050  isdrngdOLD  21051  isdrngrdOLD  21052  abvfval  21094  isabvd  21096  issrngd  21139  isorng  21145  suborng  21160  islmod  21166  islmodd  21168  scaffval  21182  lmodpropd  21227  lssset  21235  islssd  21237  prdslmodd  21271  islmhm  21329  reslmhm  21354  reslmhm2  21355  reslmhm2b  21356  islbs  21378  rlmvneg  21508  rnglidlmmgm  21560  rnglidlmsgrp  21561  rnglidlrng  21562  lsmidllsp  21564  rngqiprngghmlem3  21612  rngqiprngimfolem  21613  rngqiprnglinlem1  21614  rngqiprngimf1  21623  rngqiprnglin  21625  rng2idl1cntr  21628  rngqiprngfulem5  21638  prmidlval  21645  irinitoringc  21812  isphl  21961  ipffval  21981  isphld  21987  phssipval  21990  phssip  21991  phlssphl  21992  ocvfval  21999  isobs  22053  frlmplusgval  22097  frlmsubgval  22098  frlmvscafval  22099  frlmip  22111  frlmipval  22112  frlmup1  22131  lsslindf  22163  isassa  22191  isassad  22200  sraassab  22203  assamulgscmlem2  22235  psrval  22250  resspsradd  22309  resspsrmul  22310  resspsrvsca  22311  mplmon2mul  22405  selvvvval  22478  ply1coe  22643  ply1chr  22651  lply1binomsc  22656  evl1expd  22690  evl1scvarpw  22708  asclply1subcl  22719  mamufval  22734  matplusg2  22769  matvsca2  22770  matplusgcell  22775  matsubgcell  22776  matinvgcell  22777  matvscacell  22778  matmulcell  22787  mpomatmul  22788  mat1  22789  mattposm  22801  mat1dimmul  22818  dmatmul  22839  dmatcrng  22844  scmataddcl  22858  scmatsubcl  22859  scmatcrng  22863  smatvscl  22866  scmatghm  22875  scmatmhm  22876  mvmulfval  22884  ma1repveval  22913  mdetrlin  22944  mdetrsca  22945  mdetmul  22965  madurid  22986  minmar1cl  22993  smadiadetglem1  23013  smadiadetr  23017  matinv  23019  matunitlindflem2  23022  slesolinv  23025  slesolinvbi  23026  cramerimplem3  23030  cpmatacl  23061  mat2pmatghm  23075  decpmatmullem  23116  decpmatmul  23117  pmatcollpw1lem1  23119  pmatcollpw2lem  23122  pmatcollpwlem  23125  pmatcollpw3lem  23128  mply1topmatval  23149  mp2pm2mplem1  23151  mp2pm2mplem4  23154  mp2pm2mplem5  23155  mp2pm2mp  23156  chpmat1d  23181  chpscmatgsummon  23190  chfacfpmmulgsum2  23210  xkocnv  24160  submtmd  24450  prdsdsf  24713  ressprdsds  24717  blfvalps  24729  prdsxmslem2  24875  tmsxpsval  24884  ngpds  24950  sgrimval  24978  subgngp  24981  tngngp  25000  tngngp3  25002  isnlm  25021  lssnlm  25047  isphtpy  25329  isphtpc  25342  pi1cpbl  25392  pi1addf  25395  pi1addval  25396  pi1grplem  25397  clmsub  25428  clmvsass  25437  clmvsdir  25439  isclmp  25445  cvsdiv  25480  iscph  25518  cphdir  25553  cphdi  25554  cph2di  25555  cph2subdi  25558  cphass  25559  tcphval  25566  ipcau2  25582  tcphcphlem1  25583  tcphcphlem2  25584  cphsscph  25599  caufval  25623  rrxip  25738  rrxvsca  25742  rrxplusgvscavalb  25743  rrxdsfival  25761  ehleudisval  25767  dvlip2  26342  q1pval  26500  r1pval  26503  dvntaylp  26725  efabl  26905  efsubm  26906  dchrmul  27602  seqseq123d  28699  istrkgc  28943  istrkgb  28944  istrkgcb  28945  istrkge  28946  istrkgl  28947  istrkgld  28948  iscgrg  29002  isismt  29024  tglngval  29041  legval  29074  ishlg2  29092  ishlg  29095  mirval  29154  israg  29199  ishpg  29264  tgplnfn  29280  plngval  29282  isplng  29283  lmif  29317  islmib  29319  isinag  29384  angmgmval  29421  ttgval  29479  wksonproplem  30314  wspthsnon  30468  iswwlksnon  30469  iswspthsnon  30472  isconngr  30817  isconngr1  30818  grpodivval  31164  dipfval  31331  ipval  31332  sspgval  31358  sspsval  31360  lnoval  31381  ajfval  31438  dipdir  31471  dipass  31474  htth  31547  ressmulgnn0d  33672  inftmrel  33808  isinftm  33809  isslmd  33830  elrgspnlem1  33870  erlval  33886  rlocval  33887  rlocaddval  33897  rlocmulval  33898  subrdom  33913  resv1r  33967  idlinsubrg  34048  idlsrgval  34102  idlsrg0g  34105  rprmval  34115  ressply1evls1  34164  vietalem  34278  drgextlsp  34293  fedgmullem1  34328  fedgmullem2  34329  fedgmul  34330  extdg1id  34365  fldextrspunlsplem  34372  fldextrspunlsp  34373  extdgfialglem1  34391  extdgfialglem2  34392  algextdeglem8  34423  smatlem  34496  submatminr1  34509  metidval  34589  pstmval  34594  pstmfval  34595  zlm0  34659  zlm1  34660  sitmval  35048  breprexp  35329  istrkg2d  35362  afsval  35370  mclsrcl  36492  mppsval  36503  bj-endval  38427  istotbnd  38894  isbnd  38905  rrnequiv  38960  isrngo  39022  rngohomval  39089  idlval  39138  pridlval  39158  lflset  40307  islfld  40310  ldualvadd  40377  ldualsmul  40383  ldualvs  40385  isopos  40428  cmtfvalN  40458  iscvlat  40571  ishlat1  40600  lineset  40986  psubspset  40992  paddfval  41045  paddval  41046  ltrnfset  41365  trnfsetN  41403  trlfset  41408  tgrpov  41996  erngplus  42051  erngmul  42054  erngplus-rN  42059  erngmul-rN  42062  erngdvlem3  42238  erngdvlem4  42239  erng0g  42242  erngdvlem3-rN  42246  erngdvlem4-rN  42247  dvaplusg  42257  dvamulr  42260  dvavadd  42263  dvavsca  42265  dvalveclem  42273  dvhmulr  42334  dvhfvadd  42339  dvhvadd  42340  dvhopvadd2  42342  dvhvaddcl  42343  dvhvaddcomN  42344  dvhvsca  42349  dvhlveclem  42356  dvh0g  42359  djavalN  42383  diblsmopel  42419  dicvaddcl  42438  cdlemn6  42450  dihffval  42478  dihopelvalcpre  42496  djhval  42646  lcdvaddval  42846  lcdsmul  42850  lcdvsval  42852  lcdlkreq2N  42871  hvmapffval  43006  hvmapfval  43007  hdmap1fval  43044  hgmapffval  43133  hgmapfval  43134  hgmapadd  43142  hlhilipval  43197  hlhilhillem  43208  isprimroot  43334  aks6d1c1p4  43352  idomnnzpownz  43373  aks6d1c5lem1  43377  aks6d1c5lem3  43378  aks6d1c5lem2  43379  aks5lem3a  43430  unitscyglem5  43440  rhmpsr1  43803  mhphf2  43817  prjspval  43822  sn-isghm  43875  mnringvald  45401  ioorrnopnlem  47517  hoidmvval0b  47803  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvle  47813  ovnhoi  47816  hoiqssbl  47838  hspmbllem2  47840  vonioo  47895  vonicc  47898  zlidlring  49534  uzlidlring  49535  ovmpordxf  49654  lincop  49723  lincval  49724  lincsum  49744  lincscm  49745  lmod1lem2  49803  lmod1lem3  49804  lmod1lem4  49805  ldepsnlinc  49823  lines  50047  line  50048  rrxlines  50049  rrxline  50050  spheres  50061  ovconstbrd  50176  ovconstbrn0d  50177  elovconstbrd  50178  catprs  50328  sectrcl2  50340  invrcl2  50342  invfn  50347  isorcl2  50351  sectpropdlem  50353  invpropdlem  50355  isopropdlem  50357  cicpropdlem  50366  iinfconstbas  50383  nelsubclem  50384  nelsubc3lem  50387  ssccatid  50389  resccatlem  50390  cofu2a  50413  cofid2a  50432  cofid2  50434  cofidf2a  50436  cofidf2  50439  oppf2  50459  upfval  50495  upfval2  50496  upfval3  50497  upeu3  50514  upeu4  50515  oppcup3  50528  natoppfb  50556  swapfval  50587  swapf2a  50596  1stfpropd  50615  2ndfpropd  50616  cofuswapf2  50620  tposcurf12  50623  tposcurf2  50625  tposcurf2cl  50627  fucofvalg  50643  fuco11b  50662  fuco23a  50677  fucoaltnelem  50697  precofval3  50709  prcofpropd  50717  catcrcl2  50734  opf12  50742  fucoppcco  50747  thincmod  50768  isthincd2lem2  50773  isthincd  50774  dfinito4  50839  mndtcco2  50927  mndtccatid  50928  oppgoppchom  50931  oppgoppcco  50932  grptcmon  50934  grptcepi  50935  2arwcatlem2  50937  2arwcatlem3  50938  2arwcatlem4  50939  2arwcat  50941  parcoval  50965  lanrcl  51007  ranrcl  51008  rellan  51009  relran  51010  concom  51049  coccom  51050