Theorem oveq123d 7377

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 7373	. 2 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3		oveq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4		oveq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	oveq12d 7374	. 2 ⊢ (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
6	2, 5	eqtrd 2774	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

Syntax hints:   → wi 4   = wceq 1547  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  csbov123  7400  prdsplusgfval  17428  prdsmulrfval  17430  prdsvscafval  17434  prdsdsval2  17438  xpsaddlem  17528  xpsvsca  17532  iscat  17629  iscatd  17630  iscatd2  17638  catcocl  17642  catass  17643  moni  17694  rcaninv  17752  subccocl  17803  isfunc  17822  funcco  17829  idfucl  17839  cofuval  17840  cofuval2  17845  cofucl  17846  funcres  17854  ressffth  17898  isnat  17908  nati  17916  fuccoval  17924  coaval  18026  catcisolem  18068  xpcco  18140  xpcco2  18144  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlf2  18175  evlfcllem  18178  evlfcl  18179  curfval  18180  curf1  18182  curf12  18184  curf1cl  18185  curf2  18186  curf2val  18187  curf2cl  18188  curfcl  18189  uncfcurf  18196  hofval  18209  hof2fval  18212  hofcl  18216  yonedalem4a  18232  yonedalem3  18237  yonedainv  18238  isdlat  18479  issgrp  18679  issgrpd  18689  ismndd  18715  grpsubfval  18950  grpsubfvalALT  18951  grpsubpropd  19012  imasgrp  19023  subgsub  19105  eqgfval  19142  dpjfval  20023  isrng  20126  isrngd  20145  issrg  20160  isring  20209  isringd  20263  dvrfval  20373  isdrngd  20737  isdrngdOLD  20739  issrngd  20827  islmodd  20856  rnglidlmsgrp  21239  rnglidlrng  21240  rngqiprngimf1lem  21287  isphld  21629  phlssphl  21634  pjfval  21681  islindf  21787  isassa  21831  isassad  21840  asclfval  21853  ressascl  21871  psrval  21890  psdffval  22145  coe1tm  22259  evl1varpw  22347  evls1maplmhm  22363  scmatval  22487  mdetfval  22569  smadiadetr  22658  pmatcollpw2lem  22760  pm2mpval  22778  pm2mpghm  22799  chpmatfval  22813  cpmadugsumlemB  22857  xkohmeo  23798  xpsdsval  24364  prdsxmslem2  24512  nmfval  24571  nmpropd  24577  nmpropd2  24578  subgnm  24616  tngnm  24634  cph2di  25192  cphassr  25197  ipcau2  25219  tcphcphlem2  25221  rrxplusgvscavalb  25380  q1pval  26138  r1pval  26141  dvntaylp  26354  israg  28783  ttgval  28961  grpodivfval  30623  dipfval  30791  lnoval  30841  ressnm  33043  isslmd  33283  erlval  33339  rlocval  33340  idlinsubrg  33514  zringfrac  33637  vietalem  33763  fedgmullem2  33814  qqhval  34156  sitgval  34516  rdgeqoa  37732  prdsbnd2  38162  isrngo  38264  lflset  39551  islfld  39554  ldualset  39617  cmtfvalN  39702  isoml  39730  ltrnfset  40609  trlfset  40652  docaffvalN  41613  diblss  41662  dihffval  41722  dihfval  41723  hvmapffval  42250  hvmapfval  42251  hgmapfval  42378  isprimroot  42578  primrootsunit1  42582  aks6d1c1p4  42596  aks5lem3a  42674  imacrhmcl  43004  mendval  43624  hoidmvlelem3  47040  hspmbllem2  47070  isasslaw  48683  zlmodzxzscm  48848  lcoop  48902  lincvalsng  48907  lincvalpr  48909  lincdifsn  48915  islininds  48937  lines  49222  discsubc  49554  cofu2a  49585  cofid2  49605  cofidf2  49610  imaf1co  49645  upciclem1  49656  upfval2  49667  upfval3  49668  isuplem  49669  oppcup3lem  49696  uptrlem1  49700  uptr2  49711  swapfcoa  49771  tposcurf2val  49791  fuco21  49826  fuco23  49831  fuco22natlem3  49834  fucoid  49838  fucocolem2  49844  fucocolem4  49846  oppfdiag  49906  oppcthinendcALT  49931  isinito2lem  49988  dfinito4  49991  mndtchom  50074  mndtcco  50075  mndtccatid  50077  2arwcat  50090  setc1onsubc  50092  lanfval  50103  ranfval  50104  lanpropd  50105  ranpropd  50106  lanup  50131  ranup  50132  lmdfval  50139  cmdfval  50140  lmdpropd  50147  cmdpropd  50148  concom  50153  coccom  50154  islmd  50155  iscmd  50156  cmddu  50158