Theorem oveq123d 7452

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  csbov123  7475  prdsplusgfval  17519  prdsmulrfval  17521  prdsvscafval  17525  prdsdsval2  17529  xpsaddlem  17618  xpsvsca  17622  iscat  17715  iscatd  17716  iscatd2  17724  catcocl  17728  catass  17729  moni  17780  rcaninv  17838  subccocl  17890  isfunc  17909  funcco  17916  idfucl  17926  cofuval  17927  cofuval2  17932  cofucl  17933  funcres  17941  ressffth  17985  isnat  17995  nati  18003  fuccoval  18011  coaval  18113  catcisolem  18155  xpcco  18228  xpcco2  18232  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlf2  18263  evlfcllem  18266  evlfcl  18267  curfval  18268  curf1  18270  curf12  18272  curf1cl  18273  curf2  18274  curf2val  18275  curf2cl  18276  curfcl  18277  uncfcurf  18284  hofval  18297  hof2fval  18300  hofcl  18304  yonedalem4a  18320  yonedalem3  18325  yonedainv  18326  isdlat  18567  issgrp  18733  issgrpd  18743  ismndd  18769  grpsubfval  19001  grpsubfvalALT  19002  grpsubpropd  19063  imasgrp  19074  subgsub  19156  eqgfval  19194  dpjfval  20075  isrng  20151  isrngd  20170  issrg  20185  isring  20234  isringd  20288  dvrfval  20402  isdrngd  20765  isdrngdOLD  20767  issrngd  20856  islmodd  20864  rnglidlmsgrp  21256  rnglidlrng  21257  rngqiprngimf1lem  21304  isphld  21672  phlssphl  21677  pjfval  21726  islindf  21832  isassa  21876  isassad  21885  asclfval  21899  ressascl  21916  psrval  21935  psdffval  22161  coe1tm  22276  evl1varpw  22365  evls1maplmhm  22381  scmatval  22510  mdetfval  22592  smadiadetr  22681  pmatcollpw2lem  22783  pm2mpval  22801  pm2mpghm  22822  chpmatfval  22836  cpmadugsumlemB  22880  xkohmeo  23823  xpsdsval  24391  prdsxmslem2  24542  nmfval  24601  nmpropd  24607  nmpropd2  24608  subgnm  24646  tngnm  24672  cph2di  25241  cphassr  25246  ipcau2  25268  tcphcphlem2  25270  rrxplusgvscavalb  25429  q1pval  26194  r1pval  26197  dvntaylp  26413  israg  28705  ttgval  28883  ttgvalOLD  28884  grpodivfval  30553  dipfval  30721  lnoval  30771  ressnm  32949  isslmd  33208  erlval  33262  rlocval  33263  idlinsubrg  33459  zringfrac  33582  fedgmullem2  33681  qqhval  33973  sitgval  34334  rdgeqoa  37371  prdsbnd2  37802  isrngo  37904  lflset  39060  islfld  39063  ldualset  39126  cmtfvalN  39211  isoml  39239  ltrnfset  40119  trlfset  40162  docaffvalN  41123  diblss  41172  dihffval  41232  dihfval  41233  hvmapffval  41760  hvmapfval  41761  hgmapfval  41888  isprimroot  42094  primrootsunit1  42098  aks6d1c1p4  42112  aks5lem3a  42190  imacrhmcl  42524  mendval  43191  hoidmvlelem3  46612  hspmbllem2  46642  isasslaw  48108  zlmodzxzscm  48273  lcoop  48328  lincvalsng  48333  lincvalpr  48335  lincdifsn  48341  islininds  48363  lines  48652  upciclem1  48923  upfval2  48934  upfval3  48935  isuplem  48936  swapfcoa  48987  tposcurf2val  49001  fuco21  49031  fuco23  49036  fuco22natlem3  49039  fucoid  49043  fucocolem2  49049  fucocolem4  49051  oppcthinendcALT  49090  mndtchom  49181  mndtcco  49182  mndtccatid  49184