Theorem oveq123d 7388

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  csbov123  7411  prdsplusgfval  17437  prdsmulrfval  17439  prdsvscafval  17443  prdsdsval2  17447  xpsaddlem  17537  xpsvsca  17541  iscat  17638  iscatd  17639  iscatd2  17647  catcocl  17651  catass  17652  moni  17703  rcaninv  17761  subccocl  17812  isfunc  17831  funcco  17838  idfucl  17848  cofuval  17849  cofuval2  17854  cofucl  17855  funcres  17863  ressffth  17907  isnat  17917  nati  17925  fuccoval  17933  coaval  18035  catcisolem  18077  xpcco  18149  xpcco2  18153  1stfcl  18163  2ndfcl  18164  prfcl  18169  evlf2  18184  evlfcllem  18187  evlfcl  18188  curfval  18189  curf1  18191  curf12  18193  curf1cl  18194  curf2  18195  curf2val  18196  curf2cl  18197  curfcl  18198  uncfcurf  18205  hofval  18218  hof2fval  18221  hofcl  18225  yonedalem4a  18241  yonedalem3  18246  yonedainv  18247  isdlat  18488  issgrp  18688  issgrpd  18698  ismndd  18724  grpsubfval  18959  grpsubfvalALT  18960  grpsubpropd  19021  imasgrp  19032  subgsub  19114  eqgfval  19151  dpjfval  20032  isrng  20135  isrngd  20154  issrg  20169  isring  20218  isringd  20272  dvrfval  20382  isdrngd  20742  isdrngdOLD  20744  issrngd  20832  islmodd  20861  rnglidlmsgrp  21244  rnglidlrng  21245  rngqiprngimf1lem  21292  isphld  21634  phlssphl  21639  pjfval  21686  islindf  21792  isassa  21836  isassad  21845  asclfval  21858  ressascl  21876  psrval  21895  psdffval  22123  coe1tm  22238  evl1varpw  22326  evls1maplmhm  22342  scmatval  22469  mdetfval  22551  smadiadetr  22640  pmatcollpw2lem  22742  pm2mpval  22760  pm2mpghm  22781  chpmatfval  22795  cpmadugsumlemB  22839  xkohmeo  23780  xpsdsval  24346  prdsxmslem2  24494  nmfval  24553  nmpropd  24559  nmpropd2  24560  subgnm  24598  tngnm  24616  cph2di  25174  cphassr  25179  ipcau2  25201  tcphcphlem2  25203  rrxplusgvscavalb  25362  q1pval  26120  r1pval  26123  dvntaylp  26336  israg  28765  ttgval  28943  grpodivfval  30605  dipfval  30773  lnoval  30823  ressnm  33024  isslmd  33263  erlval  33319  rlocval  33320  idlinsubrg  33491  zringfrac  33614  vietalem  33723  fedgmullem2  33774  qqhval  34116  sitgval  34476  rdgeqoa  37686  prdsbnd2  38116  isrngo  38218  lflset  39505  islfld  39508  ldualset  39571  cmtfvalN  39656  isoml  39684  ltrnfset  40563  trlfset  40606  docaffvalN  41567  diblss  41616  dihffval  41676  dihfval  41677  hvmapffval  42204  hvmapfval  42205  hgmapfval  42332  isprimroot  42532  primrootsunit1  42536  aks6d1c1p4  42550  aks5lem3a  42628  imacrhmcl  42959  mendval  43607  hoidmvlelem3  47025  hspmbllem2  47055  isasslaw  48668  zlmodzxzscm  48833  lcoop  48887  lincvalsng  48892  lincvalpr  48894  lincdifsn  48900  islininds  48922  lines  49207  discsubc  49539  cofu2a  49570  cofid2  49590  cofidf2  49595  imaf1co  49630  upciclem1  49641  upfval2  49652  upfval3  49653  isuplem  49654  oppcup3lem  49681  uptrlem1  49685  uptr2  49696  swapfcoa  49756  tposcurf2val  49776  fuco21  49811  fuco23  49816  fuco22natlem3  49819  fucoid  49823  fucocolem2  49829  fucocolem4  49831  oppfdiag  49891  oppcthinendcALT  49916  isinito2lem  49973  dfinito4  49976  mndtchom  50059  mndtcco  50060  mndtccatid  50062  2arwcat  50075  setc1onsubc  50077  lanfval  50088  ranfval  50089  lanpropd  50090  ranpropd  50091  lanup  50116  ranup  50117  lmdfval  50124  cmdfval  50125  lmdpropd  50132  cmdpropd  50133  concom  50138  coccom  50139  islmd  50140  iscmd  50141  cmddu  50143