Theorem oveq123d 7440

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  csbov123  7463  prdsplusgfval  17551  prdsmulrfval  17553  prdsvscafval  17557  prdsdsval2  17561  xpsaddlem  17651  xpsvsca  17655  iscat  17752  iscatd  17753  iscatd2  17761  catcocl  17765  catass  17766  moni  17817  rcaninv  17875  subccocl  17926  isfunc  17945  funcco  17952  idfucl  17962  cofuval  17963  cofuval2  17968  cofucl  17969  funcres  17977  ressffth  18021  isnat  18031  nati  18039  fuccoval  18047  coaval  18149  catcisolem  18191  xpcco  18263  xpcco2  18267  1stfcl  18277  2ndfcl  18278  prfcl  18283  evlf2  18298  evlfcllem  18301  evlfcl  18302  curfval  18303  curf1  18305  curf12  18307  curf1cl  18308  curf2  18309  curf2val  18310  curf2cl  18311  curfcl  18312  uncfcurf  18319  hofval  18332  hof2fval  18335  hofcl  18339  yonedalem4a  18355  yonedalem3  18360  yonedainv  18361  isdlat  18602  issgrp  18812  issgrpd  18822  ismndd  18849  grpsubfval  19096  grpsubfvalALT  19097  grpsubpropd  19157  imasgrp  19168  subgsub  19251  eqgfval  19290  dpjfval  20173  isrng  20278  isrngd  20297  issrg  20316  isring  20365  isringd  20422  dvrfval  20532  isdrngd  20920  isdrngdOLD  20922  issrngd  21010  islmodd  21039  rnglidlmsgrp  21432  rnglidlrng  21433  rngqiprngimf1lem  21486  isphld  21856  phlssphl  21861  pjfval  21908  islindf  22014  isassa  22058  isassad  22067  asclfval  22080  ressascl  22098  psrval  22117  psdffval  22372  coe1tm  22486  evl1varpw  22573  evls1maplmhm  22589  scmatval  22713  mdetfval  22795  smadiadetr  22884  pmatcollpw2lem  22986  pm2mpval  23004  pm2mpghm  23025  chpmatfval  23039  cpmadugsumlemB  23083  xkohmeo  24025  xpsdsval  24591  prdsxmslem2  24739  nmfval  24798  nmpropd  24804  nmpropd2  24805  subgnm  24843  tngnm  24861  cph2di  25419  cphassr  25424  ipcau2  25446  tcphcphlem2  25448  rrxplusgvscavalb  25607  q1pval  26365  r1pval  26368  dvntaylp  26587  israg  29030  ttgval  29281  grpodivfval  30959  dipfval  31127  lnoval  31177  ressnm  33350  isslmd  33588  erlval  33644  rlocval  33645  idlinsubrg  33805  zringfrac  33910  vietalem  34035  fedgmullem2  34086  qqhval  34428  sitgval  34789  rdgeqoa  38075  prdsbnd2  38506  isrngo  38608  lflset  39893  islfld  39896  ldualset  39959  cmtfvalN  40044  isoml  40072  ltrnfset  40951  trlfset  40994  docaffvalN  41955  diblss  42004  dihffval  42064  dihfval  42065  hvmapffval  42592  hvmapfval  42593  hgmapfval  42720  isprimroot  42920  primrootsunit1  42924  aks6d1c1p4  42938  aks5lem3a  43016  imacrhmcl  43348  mendval  43966  hoidmvlelem3  47371  hspmbllem2  47401  isasslaw  49016  zlmodzxzscm  49196  lcoop  49250  lincvalsng  49255  lincvalpr  49257  lincdifsn  49263  islininds  49285  lines  49570  discsubc  49901  cofu2a  49932  cofid2  49952  cofidf2  49957  imaf1co  49992  upciclem1  50003  upfval2  50014  upfval3  50015  isuplem  50016  oppcup3lem  50043  uptrlem1  50047  uptr2  50058  swapfcoa  50118  tposcurf2val  50138  fuco21  50173  fuco23  50178  fuco22natlem3  50181  fucoid  50185  fucocolem2  50191  fucocolem4  50193  oppfdiag  50253  oppcthinendcALT  50278  isinito2lem  50335  dfinito4  50338  mndtchom  50421  mndtcco  50422  mndtccatid  50424  2arwcat  50437  setc1onsubc  50439  lanfval  50450  ranfval  50451  lanpropd  50452  ranpropd  50453  lanup  50478  ranup  50479  lmdfval  50486  cmdfval  50487  lmdpropd  50494  cmdpropd  50495  concom  50500  coccom  50501  islmd  50502  iscmd  50503  cmddu  50505