Theorem oveq123d 7432

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414

This theorem is referenced by:  csbov123  7453  prdsplusgfval  17422  prdsmulrfval  17424  prdsvscafval  17428  prdsdsval2  17432  xpsaddlem  17521  xpsvsca  17525  iscat  17618  iscatd  17619  iscatd2  17627  catcocl  17631  catass  17632  moni  17685  rcaninv  17743  subccocl  17797  isfunc  17816  funcco  17823  idfucl  17833  cofuval  17834  cofuval2  17839  cofucl  17840  funcres  17848  ressffth  17891  isnat  17900  nati  17908  fuccoval  17918  coaval  18020  catcisolem  18062  xpcco  18137  xpcco2  18141  1stfcl  18151  2ndfcl  18152  prfcl  18157  evlf2  18173  evlfcllem  18176  evlfcl  18177  curfval  18178  curf1  18180  curf12  18182  curf1cl  18183  curf2  18184  curf2val  18185  curf2cl  18186  curfcl  18187  uncfcurf  18194  hofval  18207  hof2fval  18210  hofcl  18214  yonedalem4a  18230  yonedalem3  18235  yonedainv  18236  isdlat  18477  issgrp  18613  issgrpd  18623  ismndd  18649  grpsubfval  18870  grpsubfvalALT  18871  grpsubpropd  18930  imasgrp  18941  subgsub  19020  eqgfval  19058  dpjfval  19927  issrg  20013  isring  20062  isringd  20107  dvrfval  20220  isdrngd  20394  isdrngdOLD  20396  issrngd  20473  islmodd  20481  isphld  21213  phlssphl  21218  pjfval  21267  islindf  21373  isassa  21417  isassad  21425  asclfval  21439  ressascl  21456  psrval  21474  coe1tm  21802  evl1varpw  21887  scmatval  22013  mdetfval  22095  smadiadetr  22184  pmatcollpw2lem  22286  pm2mpval  22304  pm2mpghm  22325  chpmatfval  22339  cpmadugsumlemB  22383  xkohmeo  23326  xpsdsval  23894  prdsxmslem2  24045  nmfval  24104  nmpropd  24110  nmpropd2  24111  subgnm  24149  tngnm  24175  cph2di  24731  cphassr  24736  ipcau2  24758  tcphcphlem2  24760  rrxplusgvscavalb  24919  q1pval  25678  r1pval  25681  dvntaylp  25890  israg  27986  ttgval  28164  ttgvalOLD  28165  grpodivfval  29825  dipfval  29993  lnoval  30043  ressnm  32166  isslmd  32388  idlinsubrg  32594  fedgmullem2  32774  evls1maplmhm  32820  qqhval  33023  sitgval  33400  rdgeqoa  36337  prdsbnd2  36749  isrngo  36851  lflset  38015  islfld  38018  ldualset  38081  cmtfvalN  38166  isoml  38194  ltrnfset  39074  trlfset  39117  docaffvalN  40078  diblss  40127  dihffval  40187  dihfval  40188  hvmapffval  40715  hvmapfval  40716  hgmapfval  40843  imacrhmcl  41173  mendval  42007  hoidmvlelem3  45392  hspmbllem2  45422  isasslaw  46681  isrng  46729  isrngd  46751  rnglidlmsgrp  46836  rnglidlrng  46837  rngqiprngimf1lem  46858  zlmodzxzscm  47112  lcoop  47170  lincvalsng  47175  lincvalpr  47177  lincdifsn  47183  islininds  47205  lines  47495  mndtchom  47788  mndtcco  47789  mndtccatid  47791