Theorem oveq123d 7379

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  csbov123  7402  prdsplusgfval  17394  prdsmulrfval  17396  prdsvscafval  17400  prdsdsval2  17404  xpsaddlem  17494  xpsvsca  17498  iscat  17595  iscatd  17596  iscatd2  17604  catcocl  17608  catass  17609  moni  17660  rcaninv  17718  subccocl  17769  isfunc  17788  funcco  17795  idfucl  17805  cofuval  17806  cofuval2  17811  cofucl  17812  funcres  17820  ressffth  17864  isnat  17874  nati  17882  fuccoval  17890  coaval  17992  catcisolem  18034  xpcco  18106  xpcco2  18110  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlf2  18141  evlfcllem  18144  evlfcl  18145  curfval  18146  curf1  18148  curf12  18150  curf1cl  18151  curf2  18152  curf2val  18153  curf2cl  18154  curfcl  18155  uncfcurf  18162  hofval  18175  hof2fval  18178  hofcl  18182  yonedalem4a  18198  yonedalem3  18203  yonedainv  18204  isdlat  18445  issgrp  18645  issgrpd  18655  ismndd  18681  grpsubfval  18913  grpsubfvalALT  18914  grpsubpropd  18975  imasgrp  18986  subgsub  19068  eqgfval  19105  dpjfval  19986  isrng  20089  isrngd  20108  issrg  20123  isring  20172  isringd  20226  dvrfval  20338  isdrngd  20698  isdrngdOLD  20700  issrngd  20788  islmodd  20817  rnglidlmsgrp  21201  rnglidlrng  21202  rngqiprngimf1lem  21249  isphld  21609  phlssphl  21614  pjfval  21661  islindf  21767  isassa  21811  isassad  21820  asclfval  21834  ressascl  21852  psrval  21871  psdffval  22100  coe1tm  22215  evl1varpw  22305  evls1maplmhm  22321  scmatval  22448  mdetfval  22530  smadiadetr  22619  pmatcollpw2lem  22721  pm2mpval  22739  pm2mpghm  22760  chpmatfval  22774  cpmadugsumlemB  22818  xkohmeo  23759  xpsdsval  24325  prdsxmslem2  24473  nmfval  24532  nmpropd  24538  nmpropd2  24539  subgnm  24577  tngnm  24595  cph2di  25163  cphassr  25168  ipcau2  25190  tcphcphlem2  25192  rrxplusgvscavalb  25351  q1pval  26116  r1pval  26119  dvntaylp  26335  israg  28769  ttgval  28947  grpodivfval  30609  dipfval  30777  lnoval  30827  ressnm  33046  isslmd  33284  erlval  33340  rlocval  33341  idlinsubrg  33512  zringfrac  33635  vietalem  33735  fedgmullem2  33787  qqhval  34129  sitgval  34489  rdgeqoa  37575  prdsbnd2  37996  isrngo  38098  lflset  39329  islfld  39332  ldualset  39395  cmtfvalN  39480  isoml  39508  ltrnfset  40387  trlfset  40430  docaffvalN  41391  diblss  41440  dihffval  41500  dihfval  41501  hvmapffval  42028  hvmapfval  42029  hgmapfval  42156  isprimroot  42357  primrootsunit1  42361  aks6d1c1p4  42375  aks5lem3a  42453  imacrhmcl  42779  mendval  43431  hoidmvlelem3  46851  hspmbllem2  46881  isasslaw  48448  zlmodzxzscm  48613  lcoop  48667  lincvalsng  48672  lincvalpr  48674  lincdifsn  48680  islininds  48702  lines  48987  discsubc  49319  cofu2a  49350  cofid2  49370  cofidf2  49375  imaf1co  49410  upciclem1  49421  upfval2  49432  upfval3  49433  isuplem  49434  oppcup3lem  49461  uptrlem1  49465  uptr2  49476  swapfcoa  49536  tposcurf2val  49556  fuco21  49591  fuco23  49596  fuco22natlem3  49599  fucoid  49603  fucocolem2  49609  fucocolem4  49611  oppfdiag  49671  oppcthinendcALT  49696  isinito2lem  49753  dfinito4  49756  mndtchom  49839  mndtcco  49840  mndtccatid  49842  2arwcat  49855  setc1onsubc  49857  lanfval  49868  ranfval  49869  lanpropd  49870  ranpropd  49871  lanup  49896  ranup  49897  lmdfval  49904  cmdfval  49905  lmdpropd  49912  cmdpropd  49913  concom  49918  coccom  49919  islmd  49920  iscmd  49921  cmddu  49923