Theorem oveq123d 7305

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

Syntax hints:   → wi 4   = wceq 1539  (class class class)co 7284

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  csbov123  7326  prdsplusgfval  17194  prdsmulrfval  17196  prdsvscafval  17200  prdsdsval2  17204  xpsaddlem  17293  xpsvsca  17297  iscat  17390  iscatd  17391  iscatd2  17399  catcocl  17403  catass  17404  moni  17457  rcaninv  17515  subccocl  17569  isfunc  17588  funcco  17595  idfucl  17605  cofuval  17606  cofuval2  17611  cofucl  17612  funcres  17620  ressffth  17663  isnat  17672  nati  17680  fuccoval  17690  coaval  17792  catcisolem  17834  xpcco  17909  xpcco2  17913  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlf2  17945  evlfcllem  17948  evlfcl  17949  curfval  17950  curf1  17952  curf12  17954  curf1cl  17955  curf2  17956  curf2val  17957  curf2cl  17958  curfcl  17959  uncfcurf  17966  hofval  17979  hof2fval  17982  hofcl  17986  yonedalem4a  18002  yonedalem3  18007  yonedainv  18008  isdlat  18249  issgrp  18385  ismndd  18416  grpsubfval  18632  grpsubfvalALT  18633  grpsubpropd  18689  imasgrp  18700  subgsub  18776  eqgfval  18813  dpjfval  19667  issrg  19752  isring  19796  isringd  19833  dvrfval  19935  isdrngd  20025  issrngd  20130  islmodd  20138  isphld  20868  phlssphl  20873  pjfval  20922  islindf  21028  isassa  21072  isassad  21080  asclfval  21092  ressascl  21109  psrval  21127  coe1tm  21453  evl1varpw  21536  scmatval  21662  mdetfval  21744  smadiadetr  21833  pmatcollpw2lem  21935  pm2mpval  21953  pm2mpghm  21974  chpmatfval  21988  cpmadugsumlemB  22032  xkohmeo  22975  xpsdsval  23543  prdsxmslem2  23694  nmfval  23753  nmpropd  23759  nmpropd2  23760  subgnm  23798  tngnm  23824  cph2di  24380  cphassr  24385  ipcau2  24407  tcphcphlem2  24409  rrxplusgvscavalb  24568  q1pval  25327  r1pval  25330  dvntaylp  25539  israg  27067  ttgval  27245  ttgvalOLD  27246  grpodivfval  28905  dipfval  29073  lnoval  29123  ressnm  31245  isslmd  31464  idlinsubrg  31617  fedgmullem2  31720  qqhval  31933  sitgval  32308  rdgeqoa  35550  prdsbnd2  35962  isrngo  36064  lflset  37080  islfld  37083  ldualset  37146  cmtfvalN  37231  isoml  37259  ltrnfset  38138  trlfset  38181  docaffvalN  39142  diblss  39191  dihffval  39251  dihfval  39252  hvmapffval  39779  hvmapfval  39780  hgmapfval  39907  mendval  41015  hoidmvlelem3  44142  hspmbllem2  44172  isasslaw  45397  isrng  45445  lidlmsgrp  45495  lidlrng  45496  zlmodzxzscm  45704  lcoop  45763  lincvalsng  45768  lincvalpr  45770  lincdifsn  45776  islininds  45798  lines  46088  mndtchom  46382  mndtcco  46383  mndtccatid  46385