Theorem oveq123d 7382

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7361

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  csbov123  7405  prdsplusgfval  17431  prdsmulrfval  17433  prdsvscafval  17437  prdsdsval2  17441  xpsaddlem  17531  xpsvsca  17535  iscat  17632  iscatd  17633  iscatd2  17641  catcocl  17645  catass  17646  moni  17697  rcaninv  17755  subccocl  17806  isfunc  17825  funcco  17832  idfucl  17842  cofuval  17843  cofuval2  17848  cofucl  17849  funcres  17857  ressffth  17901  isnat  17911  nati  17919  fuccoval  17927  coaval  18029  catcisolem  18071  xpcco  18143  xpcco2  18147  1stfcl  18157  2ndfcl  18158  prfcl  18163  evlf2  18178  evlfcllem  18181  evlfcl  18182  curfval  18183  curf1  18185  curf12  18187  curf1cl  18188  curf2  18189  curf2val  18190  curf2cl  18191  curfcl  18192  uncfcurf  18199  hofval  18212  hof2fval  18215  hofcl  18219  yonedalem4a  18235  yonedalem3  18240  yonedainv  18241  isdlat  18482  issgrp  18682  issgrpd  18692  ismndd  18718  grpsubfval  18953  grpsubfvalALT  18954  grpsubpropd  19015  imasgrp  19026  subgsub  19108  eqgfval  19145  dpjfval  20026  isrng  20129  isrngd  20148  issrg  20163  isring  20212  isringd  20266  dvrfval  20376  isdrngd  20736  isdrngdOLD  20738  issrngd  20826  islmodd  20855  rnglidlmsgrp  21239  rnglidlrng  21240  rngqiprngimf1lem  21287  isphld  21647  phlssphl  21652  pjfval  21699  islindf  21805  isassa  21849  isassad  21858  asclfval  21871  ressascl  21889  psrval  21908  psdffval  22136  coe1tm  22251  evl1varpw  22339  evls1maplmhm  22355  scmatval  22482  mdetfval  22564  smadiadetr  22653  pmatcollpw2lem  22755  pm2mpval  22773  pm2mpghm  22794  chpmatfval  22808  cpmadugsumlemB  22852  xkohmeo  23793  xpsdsval  24359  prdsxmslem2  24507  nmfval  24566  nmpropd  24572  nmpropd2  24573  subgnm  24611  tngnm  24629  cph2di  25187  cphassr  25192  ipcau2  25214  tcphcphlem2  25216  rrxplusgvscavalb  25375  q1pval  26133  r1pval  26136  dvntaylp  26351  israg  28782  ttgval  28960  grpodivfval  30623  dipfval  30791  lnoval  30841  ressnm  33042  isslmd  33281  erlval  33337  rlocval  33338  idlinsubrg  33509  zringfrac  33632  vietalem  33741  fedgmullem2  33793  qqhval  34135  sitgval  34495  rdgeqoa  37703  prdsbnd2  38133  isrngo  38235  lflset  39522  islfld  39525  ldualset  39588  cmtfvalN  39673  isoml  39701  ltrnfset  40580  trlfset  40623  docaffvalN  41584  diblss  41633  dihffval  41693  dihfval  41694  hvmapffval  42221  hvmapfval  42222  hgmapfval  42349  isprimroot  42549  primrootsunit1  42553  aks6d1c1p4  42567  aks5lem3a  42645  imacrhmcl  42976  mendval  43628  hoidmvlelem3  47046  hspmbllem2  47076  isasslaw  48683  zlmodzxzscm  48848  lcoop  48902  lincvalsng  48907  lincvalpr  48909  lincdifsn  48915  islininds  48937  lines  49222  discsubc  49554  cofu2a  49585  cofid2  49605  cofidf2  49610  imaf1co  49645  upciclem1  49656  upfval2  49667  upfval3  49668  isuplem  49669  oppcup3lem  49696  uptrlem1  49700  uptr2  49711  swapfcoa  49771  tposcurf2val  49791  fuco21  49826  fuco23  49831  fuco22natlem3  49834  fucoid  49838  fucocolem2  49844  fucocolem4  49846  oppfdiag  49906  oppcthinendcALT  49931  isinito2lem  49988  dfinito4  49991  mndtchom  50074  mndtcco  50075  mndtccatid  50077  2arwcat  50090  setc1onsubc  50092  lanfval  50103  ranfval  50104  lanpropd  50105  ranpropd  50106  lanup  50131  ranup  50132  lmdfval  50139  cmdfval  50140  lmdpropd  50147  cmdpropd  50148  concom  50153  coccom  50154  islmd  50155  iscmd  50156  cmddu  50158