Theorem oveq123d 7430

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  csbov123  7451  prdsplusgfval  17420  prdsmulrfval  17422  prdsvscafval  17426  prdsdsval2  17430  xpsaddlem  17519  xpsvsca  17523  iscat  17616  iscatd  17617  iscatd2  17625  catcocl  17629  catass  17630  moni  17683  rcaninv  17741  subccocl  17795  isfunc  17814  funcco  17821  idfucl  17831  cofuval  17832  cofuval2  17837  cofucl  17838  funcres  17846  ressffth  17889  isnat  17898  nati  17906  fuccoval  17916  coaval  18018  catcisolem  18060  xpcco  18135  xpcco2  18139  1stfcl  18149  2ndfcl  18150  prfcl  18155  evlf2  18171  evlfcllem  18174  evlfcl  18175  curfval  18176  curf1  18178  curf12  18180  curf1cl  18181  curf2  18182  curf2val  18183  curf2cl  18184  curfcl  18185  uncfcurf  18192  hofval  18205  hof2fval  18208  hofcl  18212  yonedalem4a  18228  yonedalem3  18233  yonedainv  18234  isdlat  18475  issgrp  18611  issgrpd  18621  ismndd  18647  grpsubfval  18868  grpsubfvalALT  18869  grpsubpropd  18928  imasgrp  18939  subgsub  19018  eqgfval  19056  dpjfval  19925  issrg  20011  isring  20060  isringd  20105  dvrfval  20216  isdrngd  20390  isdrngdOLD  20392  issrngd  20469  islmodd  20477  isphld  21207  phlssphl  21212  pjfval  21261  islindf  21367  isassa  21411  isassad  21419  asclfval  21433  ressascl  21450  psrval  21468  coe1tm  21795  evl1varpw  21880  scmatval  22006  mdetfval  22088  smadiadetr  22177  pmatcollpw2lem  22279  pm2mpval  22297  pm2mpghm  22318  chpmatfval  22332  cpmadugsumlemB  22376  xkohmeo  23319  xpsdsval  23887  prdsxmslem2  24038  nmfval  24097  nmpropd  24103  nmpropd2  24104  subgnm  24142  tngnm  24168  cph2di  24724  cphassr  24729  ipcau2  24751  tcphcphlem2  24753  rrxplusgvscavalb  24912  q1pval  25671  r1pval  25674  dvntaylp  25883  israg  27948  ttgval  28126  ttgvalOLD  28127  grpodivfval  29787  dipfval  29955  lnoval  30005  ressnm  32128  isslmd  32347  idlinsubrg  32549  fedgmullem2  32715  evls1maplmhm  32760  qqhval  32954  sitgval  33331  rdgeqoa  36251  prdsbnd2  36663  isrngo  36765  lflset  37929  islfld  37932  ldualset  37995  cmtfvalN  38080  isoml  38108  ltrnfset  38988  trlfset  39031  docaffvalN  39992  diblss  40041  dihffval  40101  dihfval  40102  hvmapffval  40629  hvmapfval  40630  hgmapfval  40757  imacrhmcl  41089  mendval  41925  hoidmvlelem3  45313  hspmbllem2  45343  isasslaw  46602  isrng  46650  isrngd  46672  rnglidlmsgrp  46757  rnglidlrng  46758  rngqiprngimf1lem  46779  zlmodzxzscm  47033  lcoop  47092  lincvalsng  47097  lincvalpr  47099  lincdifsn  47105  islininds  47127  lines  47417  mndtchom  47710  mndtcco  47711  mndtccatid  47713