Theorem oveq123d 7414

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

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

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 2702

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 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-iota 6484  df-fv 6540  df-ov 7396

This theorem is referenced by:  csbov123  7435  prdsplusgfval  17402  prdsmulrfval  17404  prdsvscafval  17408  prdsdsval2  17412  xpsaddlem  17501  xpsvsca  17505  iscat  17598  iscatd  17599  iscatd2  17607  catcocl  17611  catass  17612  moni  17665  rcaninv  17723  subccocl  17777  isfunc  17796  funcco  17803  idfucl  17813  cofuval  17814  cofuval2  17819  cofucl  17820  funcres  17828  ressffth  17871  isnat  17880  nati  17888  fuccoval  17898  coaval  18000  catcisolem  18042  xpcco  18117  xpcco2  18121  1stfcl  18131  2ndfcl  18132  prfcl  18137  evlf2  18153  evlfcllem  18156  evlfcl  18157  curfval  18158  curf1  18160  curf12  18162  curf1cl  18163  curf2  18164  curf2val  18165  curf2cl  18166  curfcl  18167  uncfcurf  18174  hofval  18187  hof2fval  18190  hofcl  18194  yonedalem4a  18210  yonedalem3  18215  yonedainv  18216  isdlat  18457  issgrp  18593  ismndd  18624  grpsubfval  18843  grpsubfvalALT  18844  grpsubpropd  18902  imasgrp  18913  subgsub  18990  eqgfval  19028  dpjfval  19884  issrg  19969  isring  20018  isringd  20062  dvrfval  20166  isdrngd  20297  isdrngdOLD  20299  issrngd  20418  islmodd  20426  isphld  21140  phlssphl  21145  pjfval  21194  islindf  21300  isassa  21344  isassad  21352  asclfval  21364  ressascl  21381  psrval  21399  coe1tm  21726  evl1varpw  21809  scmatval  21935  mdetfval  22017  smadiadetr  22106  pmatcollpw2lem  22208  pm2mpval  22226  pm2mpghm  22247  chpmatfval  22261  cpmadugsumlemB  22305  xkohmeo  23248  xpsdsval  23816  prdsxmslem2  23967  nmfval  24026  nmpropd  24032  nmpropd2  24033  subgnm  24071  tngnm  24097  cph2di  24653  cphassr  24658  ipcau2  24680  tcphcphlem2  24682  rrxplusgvscavalb  24841  q1pval  25600  r1pval  25603  dvntaylp  25812  israg  27813  ttgval  27991  ttgvalOLD  27992  grpodivfval  29650  dipfval  29818  lnoval  29868  ressnm  31999  isslmd  32218  idlinsubrg  32400  fedgmullem2  32553  evls1maplmhm  32597  qqhval  32785  sitgval  33162  rdgeqoa  36055  prdsbnd2  36468  isrngo  36570  lflset  37734  islfld  37737  ldualset  37800  cmtfvalN  37885  isoml  37913  ltrnfset  38793  trlfset  38836  docaffvalN  39797  diblss  39846  dihffval  39906  dihfval  39907  hvmapffval  40434  hvmapfval  40435  hgmapfval  40562  imacrhmcl  40893  mendval  41696  hoidmvlelem3  45086  hspmbllem2  45116  isasslaw  46374  isrng  46422  lidlmsgrp  46472  lidlrng  46473  zlmodzxzscm  46681  lcoop  46740  lincvalsng  46745  lincvalpr  46747  lincdifsn  46753  islininds  46775  lines  47065  mndtchom  47358  mndtcco  47359  mndtccatid  47361