Theorem oveqd 7407

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  oveq123d  7411  oveqdr  7418  csbov  7435  csbov12g  7436  ovmpodxf  7542  oprssov  7561  2mpo0  7641  ofeqd  7658  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabovd  8064  mptmpoopabbrdOLDOLD  8065  mptmpoopabovdOLD  8066  el2mpocsbcl  8067  fnmpoovd  8069  frecseq123  8264  ruclem1  16206  vdwapval  16951  vdwapid1  16953  vdwmc2  16957  vdwpc  16958  vdwlem5  16963  vdwlem8  16966  vdwlem13  16971  prdsval  17425  prdsdsval2  17454  pwsplusgval  17460  pwsmulrval  17461  pwsvscafval  17464  imasval  17481  iscat  17640  iscatd  17641  catidex  17642  catideu  17643  cidfval  17644  cidval  17645  catidd  17648  iscatd2  17649  catlid  17651  catrid  17652  homffval  17658  homfeqd  17663  homfeqval  17665  comfffval  17666  comffval  17667  comfeq  17674  comfeqd  17675  comfeqval  17676  catpropd  17677  oppcval  17681  oppcco  17685  monfval  17701  ismon  17702  oppcmon  17707  oppcepi  17708  sectffval  17719  sectfval  17720  invffval  17727  isoval  17734  dfiso2  17741  isofn  17744  invisoinvl  17759  invcoisoid  17761  isocoinvid  17762  issubc  17804  issubc3  17818  isfunc  17833  cofuval  17851  cofuval2  17856  funcres  17865  funcres2b  17866  funcres2  17867  idfusubc  17869  funcres2c  17872  isfull  17881  isfth  17885  fullres2c  17910  natfval  17918  isnat  17919  fucval  17930  fucco  17934  fucpropd  17949  initoval  17962  termoval  17963  homarcl  17997  coafval  18033  resssetc  18061  resscatc  18078  catciso  18080  xpcval  18145  1stfval  18159  2ndfval  18162  prfval  18167  prfcl  18171  evlfval  18185  curfval  18191  curf1cl  18196  curfcl  18200  uncf1  18204  uncf2  18205  diag12  18212  diag2  18213  curf2ndf  18215  hofval  18220  hof1  18222  hof2fval  18223  hofcl  18227  yon12  18233  yon2  18234  hofpropd  18235  joinval  18343  meetval  18357  isdlat  18488  plusffval  18580  ismgmd  18586  issstrmgm  18587  grpidval  18595  grpidd  18605  gsumvalx  18610  gsumpropd  18612  gsumress  18616  ismgmhm  18630  issubmgm  18636  resmgmhm  18645  resmgmhm2  18646  resmgmhm2b  18647  issgrpd  18664  ismndd  18690  issubmnd  18695  submnd0  18697  ismhm  18719  issubm  18737  resmhm  18754  resmhm2  18755  resmhm2b  18756  mhmimalem  18758  isgrp  18878  isgrpd2e  18894  grpidd2  18916  grpinvfval  18917  grpinvfvalALT  18918  imasgrp2  18994  imasgrp  18995  subg0  19071  subginv  19072  subgcl  19075  issubgrpd2  19081  isnsg  19094  isghm  19154  isghmOLD  19155  resghm  19171  isga  19230  subgga  19239  gasubg  19241  cntzfval  19259  resscntz  19272  odfval  19469  odfvalALT  19470  gexval  19515  lsmfval  19575  lsmvalx  19576  oppglsm  19579  subglsm  19610  pj1fval  19631  efgtval  19660  iscmn  19726  iscmnd  19731  submcmn2  19776  imasabl  19813  iscyg  19816  cycsubmcmn  19826  prdsmgp  20067  rngpropd  20090  ringurd  20101  issrg  20104  isring  20153  ringidss  20193  mulgass3  20269  dvdsrval  20277  rdivmuldivd  20329  isirred  20335  rnghmval  20356  islring  20456  lringuplu  20460  subrngmcl  20473  subrg1  20498  subrgdvds  20502  subrguss  20503  subrginv  20504  subrgdv  20505  subrgunit  20506  subrgugrp  20507  rnghmresel  20536  rngchom  20539  rngcco  20543  rnghmsubcsetclem1  20547  rhmresel  20565  ringchom  20568  ringcco  20572  rhmsubcsetclem1  20576  rhmsubcrngclem1  20582  rrgval  20613  isdrngd  20681  isdrngrd  20682  isdrngdOLD  20683  isdrngrdOLD  20684  abvfval  20726  isabvd  20728  issrngd  20771  islmod  20777  islmodd  20779  scaffval  20793  lmodpropd  20838  lssset  20846  islssd  20848  prdslmodd  20882  islmhm  20941  reslmhm  20966  reslmhm2  20967  reslmhm2b  20968  islbs  20990  rlmvneg  21120  rnglidlmmgm  21162  rnglidlmsgrp  21163  rnglidlrng  21164  rngqiprngghmlem3  21206  rngqiprngimfolem  21207  rngqiprnglinlem1  21208  rngqiprngimf1  21217  rngqiprnglin  21219  rng2idl1cntr  21222  rngqiprngfulem5  21232  irinitoringc  21396  isphl  21544  ipffval  21564  isphld  21570  phssipval  21573  phssip  21574  phlssphl  21575  ocvfval  21582  isobs  21636  frlmplusgval  21680  frlmsubgval  21681  frlmvscafval  21682  frlmip  21694  frlmipval  21695  frlmup1  21714  lsslindf  21746  isassa  21772  isassad  21781  sraassab  21784  assamulgscmlem2  21816  psrval  21831  resspsradd  21891  resspsrmul  21892  resspsrvsca  21893  mplmon2mul  21983  ply1coe  22192  ply1chr  22200  lply1binomsc  22205  evl1expd  22239  evl1scvarpw  22257  asclply1subcl  22268  mamufval  22286  matplusg2  22321  matvsca2  22322  matplusgcell  22327  matsubgcell  22328  matinvgcell  22329  matvscacell  22330  matmulcell  22339  mpomatmul  22340  mat1  22341  mattposm  22353  mat1dimmul  22370  dmatmul  22391  dmatcrng  22396  scmataddcl  22410  scmatsubcl  22411  scmatcrng  22415  smatvscl  22418  scmatghm  22427  scmatmhm  22428  mvmulfval  22436  ma1repveval  22465  mdetrlin  22496  mdetrsca  22497  mdetmul  22517  madurid  22538  minmar1cl  22545  smadiadetglem1  22565  smadiadetr  22569  matinv  22571  slesolinv  22574  slesolinvbi  22575  cramerimplem3  22579  cpmatacl  22610  mat2pmatghm  22624  decpmatmullem  22665  decpmatmul  22666  pmatcollpw1lem1  22668  pmatcollpw2lem  22671  pmatcollpwlem  22674  pmatcollpw3lem  22677  mply1topmatval  22698  mp2pm2mplem1  22700  mp2pm2mplem4  22703  mp2pm2mplem5  22704  mp2pm2mp  22705  chpmat1d  22730  chpscmatgsummon  22739  chfacfpmmulgsum2  22759  xkocnv  23708  submtmd  23998  prdsdsf  24262  ressprdsds  24266  blfvalps  24278  prdsxmslem2  24424  tmsxpsval  24433  ngpds  24499  sgrimval  24527  subgngp  24530  tngngp  24549  tngngp3  24551  isnlm  24570  lssnlm  24596  isphtpy  24887  isphtpc  24900  pi1cpbl  24951  pi1addf  24954  pi1addval  24955  pi1grplem  24956  clmsub  24987  clmvsass  24996  clmvsdir  24998  isclmp  25004  cvsdiv  25039  iscph  25077  cphdir  25112  cphdi  25113  cph2di  25114  cph2subdi  25117  cphass  25118  tcphval  25125  ipcau2  25141  tcphcphlem1  25142  tcphcphlem2  25143  cphsscph  25158  caufval  25182  rrxip  25297  rrxvsca  25301  rrxplusgvscavalb  25302  rrxdsfival  25320  ehleudisval  25326  dvlip2  25907  q1pval  26067  r1pval  26070  dvntaylp  26286  efabl  26466  efsubm  26467  dchrmul  27166  seqseq123d  28187  istrkgc  28388  istrkgb  28389  istrkgcb  28390  istrkge  28391  istrkgl  28392  istrkgld  28393  iscgrg  28446  isismt  28468  tglngval  28485  legval  28518  ishlg  28536  mirval  28589  israg  28631  ishpg  28693  lmif  28719  islmib  28721  isinag  28772  ttgval  28809  wksonproplem  29639  wksonproplemOLD  29640  wspthsnon  29789  iswwlksnon  29790  iswspthsnon  29793  isconngr  30125  isconngr1  30126  grpodivval  30471  dipfval  30638  ipval  30639  sspgval  30665  sspsval  30667  lnoval  30688  ajfval  30745  dipdir  30778  dipass  30781  htth  30854  ressmulgnn0d  32992  isomnd  33022  submomnd  33031  inftmrel  33141  isinftm  33142  isslmd  33162  elrgspnlem1  33200  erlval  33216  rlocval  33217  rlocaddval  33226  rlocmulval  33227  subrdom  33242  isorng  33284  suborng  33300  resv1r  33318  lsmidllsp  33378  idlinsubrg  33409  prmidlval  33415  idlsrgval  33481  idlsrg0g  33484  rprmval  33494  ressply1evls1  33541  drgextlsp  33596  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdg1id  33668  fldextrspunlsplem  33675  fldextrspunlsp  33676  algextdeglem8  33721  smatlem  33794  submatminr1  33807  metidval  33887  pstmval  33892  pstmfval  33893  zlm0  33957  zlm1  33958  sitmval  34347  breprexp  34631  istrkg2d  34664  afsval  34669  mclsrcl  35555  mppsval  35566  bj-endval  37310  matunitlindflem2  37618  istotbnd  37770  isbnd  37781  rrnequiv  37836  isrngo  37898  rngohomval  37965  idlval  38014  pridlval  38034  lflset  39059  islfld  39062  ldualvadd  39129  ldualsmul  39135  ldualvs  39137  isopos  39180  cmtfvalN  39210  iscvlat  39323  ishlat1  39352  lineset  39739  psubspset  39745  paddfval  39798  paddval  39799  ltrnfset  40118  trnfsetN  40156  trlfset  40161  tgrpov  40749  erngplus  40804  erngmul  40807  erngplus-rN  40812  erngmul-rN  40815  erngdvlem3  40991  erngdvlem4  40992  erng0g  40995  erngdvlem3-rN  40999  erngdvlem4-rN  41000  dvaplusg  41010  dvamulr  41013  dvavadd  41016  dvavsca  41018  dvalveclem  41026  dvhmulr  41087  dvhfvadd  41092  dvhvadd  41093  dvhopvadd2  41095  dvhvaddcl  41096  dvhvaddcomN  41097  dvhvsca  41102  dvhlveclem  41109  dvh0g  41112  djavalN  41136  diblsmopel  41172  dicvaddcl  41191  cdlemn6  41203  dihffval  41231  dihopelvalcpre  41249  djhval  41399  lcdvaddval  41599  lcdsmul  41603  lcdvsval  41605  lcdlkreq2N  41624  hvmapffval  41759  hvmapfval  41760  hdmap1fval  41797  hgmapffval  41886  hgmapfval  41887  hgmapadd  41895  hlhilipval  41950  hlhilhillem  41961  isprimroot  42088  aks6d1c1p4  42106  idomnnzpownz  42127  aks6d1c5lem1  42131  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks5lem3a  42184  unitscyglem5  42194  rhmpsr1  42548  selvvvval  42580  mhphf2  42593  prjspval  42598  prjspner1  42621  sn-isghm  42668  mnringvald  44209  ioorrnopnlem  46309  hoidmvval0b  46595  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvle  46605  ovnhoi  46608  hoiqssbl  46630  hspmbllem2  46632  vonioo  46687  vonicc  46690  zlidlring  48226  uzlidlring  48227  ovmpordxf  48331  lincop  48401  lincval  48402  lincsum  48422  lincscm  48423  lmod1lem2  48481  lmod1lem3  48482  lmod1lem4  48483  ldepsnlinc  48501  lines  48724  line  48725  rrxlines  48726  rrxline  48727  spheres  48739  fvconstr  48854  fvconstrn0  48855  fvconstr2  48856  catprs  49004  sectrcl2  49016  invrcl2  49018  invfn  49023  isorcl2  49027  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  cicpropdlem  49042  iinfconstbas  49059  nelsubclem  49060  nelsubc3lem  49063  ssccatid  49065  resccatlem  49066  cofu2a  49088  cofid2a  49106  cofid2  49108  cofidf2a  49110  cofidf2  49113  oppf2  49133  upfval  49169  upfval2  49170  upfval3  49171  upeu3  49188  upeu4  49189  oppcup3  49202  natoppfb  49224  swapfval  49255  swapf2a  49264  1stfpropd  49283  2ndfpropd  49284  cofuswapf2  49288  tposcurf12  49291  tposcurf2  49293  tposcurf2cl  49295  fucofvalg  49311  fuco11b  49330  fuco23a  49345  precofval3  49364  prcofpropd  49372  catcrcl2  49389  opf12  49397  fucoppcco  49402  thincmod  49423  isthincd2lem2  49428  isthincd  49429  dfinito4  49494  mndtcco2  49579  mndtccatid  49580  oppgoppchom  49583  oppgoppcco  49584  grptcmon  49586  grptcepi  49587  2arwcatlem2  49589  2arwcatlem3  49590  2arwcatlem4  49591  2arwcat  49593  lanrcl  49614  ranrcl  49615  rellan  49616  relran  49617  concom  49656  coccom  49657