Theorem oveq123d 7367

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

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7346

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  csbov123  7390  prdsplusgfval  17378  prdsmulrfval  17380  prdsvscafval  17384  prdsdsval2  17388  xpsaddlem  17477  xpsvsca  17481  iscat  17578  iscatd  17579  iscatd2  17587  catcocl  17591  catass  17592  moni  17643  rcaninv  17701  subccocl  17752  isfunc  17771  funcco  17778  idfucl  17788  cofuval  17789  cofuval2  17794  cofucl  17795  funcres  17803  ressffth  17847  isnat  17857  nati  17865  fuccoval  17873  coaval  17975  catcisolem  18017  xpcco  18089  xpcco2  18093  1stfcl  18103  2ndfcl  18104  prfcl  18109  evlf2  18124  evlfcllem  18127  evlfcl  18128  curfval  18129  curf1  18131  curf12  18133  curf1cl  18134  curf2  18135  curf2val  18136  curf2cl  18137  curfcl  18138  uncfcurf  18145  hofval  18158  hof2fval  18161  hofcl  18165  yonedalem4a  18181  yonedalem3  18186  yonedainv  18187  isdlat  18428  issgrp  18628  issgrpd  18638  ismndd  18664  grpsubfval  18896  grpsubfvalALT  18897  grpsubpropd  18958  imasgrp  18969  subgsub  19051  eqgfval  19088  dpjfval  19969  isrng  20072  isrngd  20091  issrg  20106  isring  20155  isringd  20209  dvrfval  20320  isdrngd  20680  isdrngdOLD  20682  issrngd  20770  islmodd  20799  rnglidlmsgrp  21183  rnglidlrng  21184  rngqiprngimf1lem  21231  isphld  21591  phlssphl  21596  pjfval  21643  islindf  21749  isassa  21793  isassad  21802  asclfval  21816  ressascl  21833  psrval  21852  psdffval  22072  coe1tm  22187  evl1varpw  22276  evls1maplmhm  22292  scmatval  22419  mdetfval  22501  smadiadetr  22590  pmatcollpw2lem  22692  pm2mpval  22710  pm2mpghm  22731  chpmatfval  22745  cpmadugsumlemB  22789  xkohmeo  23730  xpsdsval  24296  prdsxmslem2  24444  nmfval  24503  nmpropd  24509  nmpropd2  24510  subgnm  24548  tngnm  24566  cph2di  25134  cphassr  25139  ipcau2  25161  tcphcphlem2  25163  rrxplusgvscavalb  25322  q1pval  26087  r1pval  26090  dvntaylp  26306  israg  28675  ttgval  28853  grpodivfval  30514  dipfval  30682  lnoval  30732  ressnm  32945  isslmd  33171  erlval  33225  rlocval  33226  idlinsubrg  33396  zringfrac  33519  fedgmullem2  33643  qqhval  33985  sitgval  34345  rdgeqoa  37414  prdsbnd2  37845  isrngo  37947  lflset  39168  islfld  39171  ldualset  39234  cmtfvalN  39319  isoml  39347  ltrnfset  40226  trlfset  40269  docaffvalN  41230  diblss  41279  dihffval  41339  dihfval  41340  hvmapffval  41867  hvmapfval  41868  hgmapfval  41995  isprimroot  42196  primrootsunit1  42200  aks6d1c1p4  42214  aks5lem3a  42292  imacrhmcl  42617  mendval  43282  hoidmvlelem3  46705  hspmbllem2  46735  isasslaw  48302  zlmodzxzscm  48467  lcoop  48522  lincvalsng  48527  lincvalpr  48529  lincdifsn  48535  islininds  48557  lines  48842  discsubc  49175  cofu2a  49206  cofid2  49226  cofidf2  49231  imaf1co  49266  upciclem1  49277  upfval2  49288  upfval3  49289  isuplem  49290  oppcup3lem  49317  uptrlem1  49321  uptr2  49332  swapfcoa  49392  tposcurf2val  49412  fuco21  49447  fuco23  49452  fuco22natlem3  49455  fucoid  49459  fucocolem2  49465  fucocolem4  49467  oppfdiag  49527  oppcthinendcALT  49552  isinito2lem  49609  dfinito4  49612  mndtchom  49695  mndtcco  49696  mndtccatid  49698  2arwcat  49711  setc1onsubc  49713  lanfval  49724  ranfval  49725  lanpropd  49726  ranpropd  49727  lanup  49752  ranup  49753  lmdfval  49760  cmdfval  49761  lmdpropd  49768  cmdpropd  49769  concom  49774  coccom  49775  islmd  49776  iscmd  49777  cmddu  49779