Theorem oveq123d 7451

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

Syntax hints:   → wi 4   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  csbov123  7474  prdsplusgfval  17520  prdsmulrfval  17522  prdsvscafval  17526  prdsdsval2  17530  xpsaddlem  17619  xpsvsca  17623  iscat  17716  iscatd  17717  iscatd2  17725  catcocl  17729  catass  17730  moni  17783  rcaninv  17841  subccocl  17895  isfunc  17914  funcco  17921  idfucl  17931  cofuval  17932  cofuval2  17937  cofucl  17938  funcres  17946  ressffth  17991  isnat  18001  nati  18009  fuccoval  18019  coaval  18121  catcisolem  18163  xpcco  18238  xpcco2  18242  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlf2  18274  evlfcllem  18277  evlfcl  18278  curfval  18279  curf1  18281  curf12  18283  curf1cl  18284  curf2  18285  curf2val  18286  curf2cl  18287  curfcl  18288  uncfcurf  18295  hofval  18308  hof2fval  18311  hofcl  18315  yonedalem4a  18331  yonedalem3  18336  yonedainv  18337  isdlat  18579  issgrp  18745  issgrpd  18755  ismndd  18781  grpsubfval  19013  grpsubfvalALT  19014  grpsubpropd  19075  imasgrp  19086  subgsub  19168  eqgfval  19206  dpjfval  20089  isrng  20171  isrngd  20190  issrg  20205  isring  20254  isringd  20304  dvrfval  20418  isdrngd  20781  isdrngdOLD  20783  issrngd  20872  islmodd  20880  rnglidlmsgrp  21273  rnglidlrng  21274  rngqiprngimf1lem  21321  isphld  21689  phlssphl  21694  pjfval  21743  islindf  21849  isassa  21893  isassad  21902  asclfval  21916  ressascl  21933  psrval  21952  psdffval  22178  coe1tm  22291  evl1varpw  22380  evls1maplmhm  22396  scmatval  22525  mdetfval  22607  smadiadetr  22696  pmatcollpw2lem  22798  pm2mpval  22816  pm2mpghm  22837  chpmatfval  22851  cpmadugsumlemB  22895  xkohmeo  23838  xpsdsval  24406  prdsxmslem2  24557  nmfval  24616  nmpropd  24622  nmpropd2  24623  subgnm  24661  tngnm  24687  cph2di  25254  cphassr  25259  ipcau2  25281  tcphcphlem2  25283  rrxplusgvscavalb  25442  q1pval  26208  r1pval  26211  dvntaylp  26427  israg  28719  ttgval  28897  ttgvalOLD  28898  grpodivfval  30562  dipfval  30730  lnoval  30780  ressnm  32933  isslmd  33190  erlval  33244  rlocval  33245  idlinsubrg  33438  zringfrac  33561  fedgmullem2  33657  qqhval  33934  sitgval  34313  rdgeqoa  37352  prdsbnd2  37781  isrngo  37883  lflset  39040  islfld  39043  ldualset  39106  cmtfvalN  39191  isoml  39219  ltrnfset  40099  trlfset  40142  docaffvalN  41103  diblss  41152  dihffval  41212  dihfval  41213  hvmapffval  41740  hvmapfval  41741  hgmapfval  41868  isprimroot  42074  primrootsunit1  42078  aks6d1c1p4  42092  aks5lem3a  42170  imacrhmcl  42500  mendval  43167  hoidmvlelem3  46552  hspmbllem2  46582  isasslaw  48035  zlmodzxzscm  48201  lcoop  48256  lincvalsng  48261  lincvalpr  48263  lincdifsn  48269  islininds  48291  lines  48580  upciclem1  48811  mndtchom  48892  mndtcco  48893  mndtccatid  48895