Theorem oveqd 7175

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  oveq123d  7179  oveqdr  7186  csbov  7201  csbov12g  7202  ovmpodxf  7302  oprssov  7319  2mpo0  7396  ofeq  7413  mptmpoopabbrd  7780  mptmpoopabovd  7781  el2mpocsbcl  7782  fnmpoovd  7784  ruclem1  15586  vdwapval  16311  vdwapid1  16313  vdwmc2  16317  vdwpc  16318  vdwlem5  16323  vdwlem8  16326  vdwlem13  16331  prdsval  16730  prdsdsval2  16759  pwsplusgval  16765  pwsmulrval  16766  pwsvscafval  16769  imasval  16786  iscat  16945  iscatd  16946  catidex  16947  catideu  16948  cidfval  16949  cidval  16950  catidd  16953  iscatd2  16954  catlid  16956  catrid  16957  homffval  16962  homfeqd  16967  homfeqval  16969  comfffval  16970  comffval  16971  comfeq  16978  comfeqd  16979  comfeqval  16980  catpropd  16981  oppcval  16985  oppcco  16989  monfval  17004  ismon  17005  oppcmon  17010  oppcepi  17011  sectffval  17022  sectfval  17023  invffval  17030  isoval  17037  dfiso2  17044  isofn  17047  invisoinvl  17062  invcoisoid  17064  isocoinvid  17065  issubc  17107  issubc3  17121  isfunc  17136  cofuval  17154  cofuval2  17159  funcres  17168  funcres2b  17169  funcres2  17170  funcres2c  17173  isfull  17182  isfth  17186  fullres2c  17211  natfval  17218  isnat  17219  fucval  17230  fucco  17234  fucpropd  17249  initoval  17259  termoval  17260  homarcl  17290  coafval  17326  resssetc  17354  resscatc  17367  catciso  17369  xpcval  17429  1stfval  17443  2ndfval  17446  prfval  17451  prfcl  17455  evlfval  17469  curfval  17475  curf1cl  17480  curfcl  17484  uncf1  17488  uncf2  17489  diag12  17496  diag2  17497  curf2ndf  17499  hofval  17504  hof1  17506  hof2fval  17507  hofcl  17511  yon12  17517  yon2  17518  hofpropd  17519  joinval  17617  meetval  17631  isdlat  17805  plusffval  17860  issstrmgm  17865  grpidval  17873  grpidd  17883  gsumvalx  17888  gsumpropd  17890  gsumress  17894  ismndd  17935  issubmnd  17940  submnd0  17942  ismhm  17960  issubm  17970  resmhm  17987  resmhm2  17988  resmhm2b  17989  isgrp  18111  isgrpd2e  18124  grpidd2  18143  grpinvfval  18144  grpinvfvalALT  18145  imasgrp2  18216  imasgrp  18217  subg0  18287  subginv  18288  subgcl  18291  issubgrpd2  18297  isnsg  18309  isghm  18360  resghm  18376  isga  18423  subgga  18432  gasubg  18434  cntzfval  18452  resscntz  18464  odfval  18662  odfvalALT  18663  gexval  18705  lsmfval  18765  lsmvalx  18766  oppglsm  18769  subglsm  18801  pj1fval  18822  efgtval  18851  iscmn  18916  iscmnd  18921  submcmn2  18961  iscyg  19000  cycsubmcmn  19010  issrg  19259  isring  19303  ringidss  19329  prdsmgp  19362  mulgass3  19389  dvdsrval  19397  isirred  19451  isdrngd  19529  isdrngrd  19530  subrg1  19547  subrgmcl  19549  subrgdvds  19551  subrguss  19552  subrginv  19553  subrgdv  19554  subrgunit  19555  subrgugrp  19556  abvfval  19591  isabvd  19593  issrngd  19634  islmod  19640  islmodd  19642  scaffval  19654  lmodpropd  19699  lssset  19707  islssd  19709  prdslmodd  19743  islmhm  19801  reslmhm  19826  reslmhm2  19827  reslmhm2b  19828  islbs  19850  rlmvneg  19982  rrgval  20062  isassa  20090  isassad  20098  assamulgscmlem2  20131  psrval  20144  resspsradd  20198  resspsrmul  20199  resspsrvsca  20200  mplmon2mul  20283  ply1coe  20466  lply1binomsc  20477  evl1expd  20510  evl1scvarpw  20528  isphl  20774  ipffval  20794  isphld  20800  phssipval  20803  phssip  20804  phlssphl  20805  ocvfval  20812  isobs  20866  frlmplusgval  20910  frlmsubgval  20911  frlmvscafval  20912  frlmip  20924  frlmipval  20925  frlmup1  20944  lsslindf  20976  mamufval  20998  matplusg2  21038  matvsca2  21039  matplusgcell  21044  matsubgcell  21045  matinvgcell  21046  matvscacell  21047  matmulcell  21056  mpomatmul  21057  mat1  21058  mattposm  21070  mat1dimmul  21087  dmatmul  21108  dmatcrng  21113  scmataddcl  21127  scmatsubcl  21128  scmatcrng  21132  smatvscl  21135  scmatghm  21144  scmatmhm  21145  mvmulfval  21153  ma1repveval  21182  mdetrlin  21213  mdetrsca  21214  mdetmul  21234  madurid  21255  minmar1cl  21262  smadiadetglem1  21282  smadiadetr  21286  matinv  21288  slesolinv  21291  slesolinvbi  21292  cramerimplem3  21296  cpmatacl  21326  mat2pmatghm  21340  decpmatmullem  21381  decpmatmul  21382  pmatcollpw1lem1  21384  pmatcollpw2lem  21387  pmatcollpwlem  21390  pmatcollpw3lem  21393  mply1topmatval  21414  mp2pm2mplem1  21416  mp2pm2mplem4  21419  mp2pm2mplem5  21420  mp2pm2mp  21421  chpmat1d  21446  chpscmatgsummon  21455  chfacfpmmulgsum2  21475  xkocnv  22424  submtmd  22714  prdsdsf  22979  ressprdsds  22983  blfvalps  22995  prdsxmslem2  23141  tmsxpsval  23150  ngpds  23215  sgrimval  23243  subgngp  23246  tngngp  23265  tngngp3  23267  isnlm  23286  lssnlm  23312  isphtpy  23587  isphtpc  23600  pi1cpbl  23650  pi1addf  23653  pi1addval  23654  pi1grplem  23655  clmsub  23686  clmvsass  23695  clmvsdir  23697  isclmp  23703  cvsdiv  23738  iscph  23776  cphdir  23811  cphdi  23812  cph2di  23813  cph2subdi  23816  cphass  23817  tcphval  23823  ipcau2  23839  tcphcphlem1  23840  tcphcphlem2  23841  cphsscph  23856  caufval  23880  rrxip  23995  rrxvsca  23999  rrxplusgvscavalb  24000  rrxdsfival  24018  ehleudisval  24024  dvlip2  24594  q1pval  24749  r1pval  24752  dvntaylp  24961  efabl  25136  efsubm  25137  dchrmul  25826  istrkgc  26242  istrkgb  26243  istrkgcb  26244  istrkge  26245  istrkgl  26246  istrkgld  26247  iscgrg  26300  isismt  26322  tglngval  26339  legval  26372  ishlg  26390  mirval  26443  israg  26485  ishpg  26547  lmif  26573  islmib  26575  isinag  26626  ttgval  26663  wksonproplem  27488  wspthsnon  27632  iswwlksnon  27633  iswspthsnon  27636  isconngr  27970  isconngr1  27971  grpodivval  28314  dipfval  28481  ipval  28482  sspgval  28508  sspsval  28510  lnoval  28531  ajfval  28588  dipdir  28621  dipass  28624  htth  28697  isomnd  30704  submomnd  30713  inftmrel  30811  isinftm  30812  isslmd  30832  rngurd  30859  rdivmuldivd  30864  isorng  30874  suborng  30890  resv1r  30912  lsmidllsp  30952  prmidlval  30956  drgextlsp  30998  fedgmullem1  31027  fedgmullem2  31028  fedgmul  31029  extdg1id  31055  smatlem  31064  submatminr1  31077  metidval  31132  pstmval  31137  pstmfval  31138  zlm0  31205  zlm1  31206  sitmval  31609  breprexp  31906  istrkg2d  31939  afsval  31944  mclsrcl  32810  mppsval  32821  frecseq123  33121  bj-endval  34598  matunitlindflem2  34891  istotbnd  35049  isbnd  35060  rrnequiv  35115  isrngo  35177  rngohomval  35244  idlval  35293  pridlval  35313  lflset  36197  islfld  36200  ldualvadd  36267  ldualsmul  36273  ldualvs  36275  isopos  36318  cmtfvalN  36348  iscvlat  36461  ishlat1  36490  lineset  36876  psubspset  36882  paddfval  36935  paddval  36936  ltrnfset  37255  trnfsetN  37293  trlfset  37298  tgrpov  37886  erngplus  37941  erngmul  37944  erngplus-rN  37949  erngmul-rN  37952  erngdvlem3  38128  erngdvlem4  38129  erng0g  38132  erngdvlem3-rN  38136  erngdvlem4-rN  38137  dvaplusg  38147  dvamulr  38150  dvavadd  38153  dvavsca  38155  dvalveclem  38163  dvhmulr  38224  dvhfvadd  38229  dvhvadd  38230  dvhopvadd2  38232  dvhvaddcl  38233  dvhvaddcomN  38234  dvhvsca  38239  dvhlveclem  38246  dvh0g  38249  djavalN  38273  diblsmopel  38309  dicvaddcl  38328  cdlemn6  38340  dihffval  38368  dihopelvalcpre  38386  djhval  38536  lcdvaddval  38736  lcdsmul  38740  lcdvsval  38742  lcdlkreq2N  38761  hvmapffval  38896  hvmapfval  38897  hdmap1fval  38934  hgmapffval  39023  hgmapfval  39024  hgmapadd  39032  hlhilipval  39087  hlhilhillem  39098  prjspval  39260  ioorrnopnlem  42596  hoidmvval0b  42879  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvle  42889  ovnhoi  42892  hoiqssbl  42914  hspmbllem2  42916  vonioo  42971  vonicc  42974  ismgmd  44050  ismgmhm  44057  issubmgm  44063  resmgmhm  44072  resmgmhm2  44073  resmgmhm2b  44074  idfusubc  44144  rnghmval  44169  lidlmsgrp  44204  lidlrng  44205  zlidlring  44206  uzlidlring  44207  rnghmresel  44242  rngchom  44245  rngcco  44249  rnghmsubcsetclem1  44253  rhmresel  44288  ringchom  44291  ringcco  44295  rhmsubcsetclem1  44299  rhmsubcrngclem1  44305  irinitoringc  44347  ovmpordxf  44394  lincop  44470  lincval  44471  lincsum  44491  lincscm  44492  lmod1lem2  44550  lmod1lem3  44551  lmod1lem4  44552  ldepsnlinc  44570  lines  44725  line  44726  rrxlines  44727  rrxline  44728  spheres  44740