Theorem oveq123d 7370

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  csbov123  7393  prdsplusgfval  17378  prdsmulrfval  17380  prdsvscafval  17384  prdsdsval2  17388  xpsaddlem  17477  xpsvsca  17481  iscat  17578  iscatd  17579  iscatd2  17587  catcocl  17591  catass  17592  moni  17643  rcaninv  17701  subccocl  17752  isfunc  17771  funcco  17778  idfucl  17788  cofuval  17789  cofuval2  17794  cofucl  17795  funcres  17803  ressffth  17847  isnat  17857  nati  17865  fuccoval  17873  coaval  17975  catcisolem  18017  xpcco  18089  xpcco2  18093  1stfcl  18103  2ndfcl  18104  prfcl  18109  evlf2  18124  evlfcllem  18127  evlfcl  18128  curfval  18129  curf1  18131  curf12  18133  curf1cl  18134  curf2  18135  curf2val  18136  curf2cl  18137  curfcl  18138  uncfcurf  18145  hofval  18158  hof2fval  18161  hofcl  18165  yonedalem4a  18181  yonedalem3  18186  yonedainv  18187  isdlat  18428  issgrp  18594  issgrpd  18604  ismndd  18630  grpsubfval  18862  grpsubfvalALT  18863  grpsubpropd  18924  imasgrp  18935  subgsub  19017  eqgfval  19055  dpjfval  19936  isrng  20039  isrngd  20058  issrg  20073  isring  20122  isringd  20176  dvrfval  20287  isdrngd  20650  isdrngdOLD  20652  issrngd  20740  islmodd  20769  rnglidlmsgrp  21153  rnglidlrng  21154  rngqiprngimf1lem  21201  isphld  21561  phlssphl  21566  pjfval  21613  islindf  21719  isassa  21763  isassad  21772  asclfval  21786  ressascl  21803  psrval  21822  psdffval  22042  coe1tm  22157  evl1varpw  22246  evls1maplmhm  22262  scmatval  22389  mdetfval  22471  smadiadetr  22560  pmatcollpw2lem  22662  pm2mpval  22680  pm2mpghm  22701  chpmatfval  22715  cpmadugsumlemB  22759  xkohmeo  23700  xpsdsval  24267  prdsxmslem2  24415  nmfval  24474  nmpropd  24480  nmpropd2  24481  subgnm  24519  tngnm  24537  cph2di  25105  cphassr  25110  ipcau2  25132  tcphcphlem2  25134  rrxplusgvscavalb  25293  q1pval  26058  r1pval  26061  dvntaylp  26277  israg  28642  ttgval  28820  grpodivfval  30478  dipfval  30646  lnoval  30696  ressnm  32906  isslmd  33144  erlval  33198  rlocval  33199  idlinsubrg  33368  zringfrac  33491  fedgmullem2  33597  qqhval  33939  sitgval  34300  rdgeqoa  37348  prdsbnd2  37779  isrngo  37881  lflset  39042  islfld  39045  ldualset  39108  cmtfvalN  39193  isoml  39221  ltrnfset  40100  trlfset  40143  docaffvalN  41104  diblss  41153  dihffval  41213  dihfval  41214  hvmapffval  41741  hvmapfval  41742  hgmapfval  41869  isprimroot  42070  primrootsunit1  42074  aks6d1c1p4  42088  aks5lem3a  42166  imacrhmcl  42491  mendval  43156  hoidmvlelem3  46582  hspmbllem2  46612  isasslaw  48180  zlmodzxzscm  48345  lcoop  48400  lincvalsng  48405  lincvalpr  48407  lincdifsn  48413  islininds  48435  lines  48720  discsubc  49053  cofu2a  49084  cofid2  49104  cofidf2  49109  imaf1co  49144  upciclem1  49155  upfval2  49166  upfval3  49167  isuplem  49168  oppcup3lem  49195  uptrlem1  49199  uptr2  49210  swapfcoa  49270  tposcurf2val  49290  fuco21  49325  fuco23  49330  fuco22natlem3  49333  fucoid  49337  fucocolem2  49343  fucocolem4  49345  oppfdiag  49405  oppcthinendcALT  49430  isinito2lem  49487  dfinito4  49490  mndtchom  49573  mndtcco  49574  mndtccatid  49576  2arwcat  49589  setc1onsubc  49591  lanfval  49602  ranfval  49603  lanpropd  49604  ranpropd  49605  lanup  49630  ranup  49631  lmdfval  49638  cmdfval  49639  lmdpropd  49646  cmdpropd  49647  concom  49652  coccom  49653  islmd  49654  iscmd  49655  cmddu  49657