Theorem oveq123d 7417

Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)

Hypotheses

Ref	Expression
oveq123d.1	⊢ (𝜑 → 𝐹 = 𝐺)
oveq123d.2	⊢ (𝜑 → 𝐴 = 𝐵)
oveq123d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
oveq123d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

Proof of Theorem oveq123d

Step	Hyp	Ref	Expression
1		oveq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	oveqd 7413	. 2 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3		oveq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4		oveq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	oveq12d 7414	. 2 ⊢ (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
6	2, 5	eqtrd 2797	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

Syntax hints:   → wi 4   = wceq 1560  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  csbov123  7440  prdsplusgfval  17503  prdsmulrfval  17505  prdsvscafval  17509  prdsdsval2  17513  xpsaddlem  17603  xpsvsca  17607  iscat  17704  iscatd  17705  iscatd2  17713  catcocl  17717  catass  17718  moni  17769  rcaninv  17827  subccocl  17878  isfunc  17897  funcco  17904  idfucl  17914  cofuval  17915  cofuval2  17920  cofucl  17921  funcres  17929  ressffth  17973  isnat  17983  nati  17991  fuccoval  17999  coaval  18101  catcisolem  18143  xpcco  18215  xpcco2  18219  1stfcl  18229  2ndfcl  18230  prfcl  18235  evlf2  18250  evlfcllem  18253  evlfcl  18254  curfval  18255  curf1  18257  curf12  18259  curf1cl  18260  curf2  18261  curf2val  18262  curf2cl  18263  curfcl  18264  uncfcurf  18271  hofval  18284  hof2fval  18287  hofcl  18291  yonedalem4a  18307  yonedalem3  18312  yonedainv  18313  isdlat  18554  issgrp  18754  issgrpd  18764  ismndd  18790  grpsubfval  19025  grpsubfvalALT  19026  grpsubpropd  19087  imasgrp  19098  subgsub  19180  eqgfval  19217  dpjfval  20097  isrng  20200  isrngd  20219  issrg  20238  isring  20287  isringd  20341  dvrfval  20451  isdrngd  20815  isdrngdOLD  20817  issrngd  20904  islmodd  20933  rnglidlmsgrp  21316  rnglidlrng  21317  rngqiprngimf1lem  21364  isphld  21706  phlssphl  21711  pjfval  21758  islindf  21864  isassa  21908  isassad  21917  asclfval  21930  ressascl  21948  psrval  21967  psdffval  22222  coe1tm  22336  evl1varpw  22424  evls1maplmhm  22440  scmatval  22564  mdetfval  22646  smadiadetr  22735  pmatcollpw2lem  22837  pm2mpval  22855  pm2mpghm  22876  chpmatfval  22890  cpmadugsumlemB  22934  xkohmeo  23875  xpsdsval  24441  prdsxmslem2  24589  nmfval  24648  nmpropd  24654  nmpropd2  24655  subgnm  24693  tngnm  24711  cph2di  25269  cphassr  25274  ipcau2  25296  tcphcphlem2  25298  rrxplusgvscavalb  25457  q1pval  26215  r1pval  26218  dvntaylp  26434  israg  28870  ttgval  29075  grpodivfval  30737  dipfval  30905  lnoval  30955  ressnm  33142  isslmd  33382  erlval  33439  rlocval  33440  idlinsubrg  33617  zringfrac  33750  vietalem  33876  fedgmullem2  33927  qqhval  34269  sitgval  34629  rdgeqoa  37864  prdsbnd2  38294  isrngo  38396  lflset  39683  islfld  39686  ldualset  39749  cmtfvalN  39834  isoml  39862  ltrnfset  40741  trlfset  40784  docaffvalN  41745  diblss  41794  dihffval  41854  dihfval  41855  hvmapffval  42382  hvmapfval  42383  hgmapfval  42510  isprimroot  42710  primrootsunit1  42714  aks6d1c1p4  42728  aks5lem3a  42806  imacrhmcl  43136  mendval  43756  hoidmvlelem3  47171  hspmbllem2  47201  isasslaw  48814  zlmodzxzscm  48979  lcoop  49033  lincvalsng  49038  lincvalpr  49040  lincdifsn  49046  islininds  49068  lines  49353  discsubc  49685  cofu2a  49716  cofid2  49736  cofidf2  49741  imaf1co  49776  upciclem1  49787  upfval2  49798  upfval3  49799  isuplem  49800  oppcup3lem  49827  uptrlem1  49831  uptr2  49842  swapfcoa  49902  tposcurf2val  49922  fuco21  49957  fuco23  49962  fuco22natlem3  49965  fucoid  49969  fucocolem2  49975  fucocolem4  49977  oppfdiag  50037  oppcthinendcALT  50062  isinito2lem  50119  dfinito4  50122  mndtchom  50205  mndtcco  50206  mndtccatid  50208  2arwcat  50221  setc1onsubc  50223  lanfval  50234  ranfval  50235  lanpropd  50236  ranpropd  50237  lanup  50262  ranup  50263  lmdfval  50270  cmdfval  50271  lmdpropd  50278  cmdpropd  50279  concom  50284  coccom  50285  islmd  50286  iscmd  50287  cmddu  50289