Theorem oveq123d 7389

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  csbov123  7412  prdsplusgfval  17406  prdsmulrfval  17408  prdsvscafval  17412  prdsdsval2  17416  xpsaddlem  17506  xpsvsca  17510  iscat  17607  iscatd  17608  iscatd2  17616  catcocl  17620  catass  17621  moni  17672  rcaninv  17730  subccocl  17781  isfunc  17800  funcco  17807  idfucl  17817  cofuval  17818  cofuval2  17823  cofucl  17824  funcres  17832  ressffth  17876  isnat  17886  nati  17894  fuccoval  17902  coaval  18004  catcisolem  18046  xpcco  18118  xpcco2  18122  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlf2  18153  evlfcllem  18156  evlfcl  18157  curfval  18158  curf1  18160  curf12  18162  curf1cl  18163  curf2  18164  curf2val  18165  curf2cl  18166  curfcl  18167  uncfcurf  18174  hofval  18187  hof2fval  18190  hofcl  18194  yonedalem4a  18210  yonedalem3  18215  yonedainv  18216  isdlat  18457  issgrp  18657  issgrpd  18667  ismndd  18693  grpsubfval  18925  grpsubfvalALT  18926  grpsubpropd  18987  imasgrp  18998  subgsub  19080  eqgfval  19117  dpjfval  19998  isrng  20101  isrngd  20120  issrg  20135  isring  20184  isringd  20238  dvrfval  20350  isdrngd  20710  isdrngdOLD  20712  issrngd  20800  islmodd  20829  rnglidlmsgrp  21213  rnglidlrng  21214  rngqiprngimf1lem  21261  isphld  21621  phlssphl  21626  pjfval  21673  islindf  21779  isassa  21823  isassad  21832  asclfval  21846  ressascl  21864  psrval  21883  psdffval  22112  coe1tm  22227  evl1varpw  22317  evls1maplmhm  22333  scmatval  22460  mdetfval  22542  smadiadetr  22631  pmatcollpw2lem  22733  pm2mpval  22751  pm2mpghm  22772  chpmatfval  22786  cpmadugsumlemB  22830  xkohmeo  23771  xpsdsval  24337  prdsxmslem2  24485  nmfval  24544  nmpropd  24550  nmpropd2  24551  subgnm  24589  tngnm  24607  cph2di  25175  cphassr  25180  ipcau2  25202  tcphcphlem2  25204  rrxplusgvscavalb  25363  q1pval  26128  r1pval  26131  dvntaylp  26347  israg  28781  ttgval  28959  grpodivfval  30622  dipfval  30790  lnoval  30840  ressnm  33057  isslmd  33296  erlval  33352  rlocval  33353  idlinsubrg  33524  zringfrac  33647  vietalem  33756  fedgmullem2  33808  qqhval  34150  sitgval  34510  rdgeqoa  37625  prdsbnd2  38046  isrngo  38148  lflset  39435  islfld  39438  ldualset  39501  cmtfvalN  39586  isoml  39614  ltrnfset  40493  trlfset  40536  docaffvalN  41497  diblss  41546  dihffval  41606  dihfval  41607  hvmapffval  42134  hvmapfval  42135  hgmapfval  42262  isprimroot  42463  primrootsunit1  42467  aks6d1c1p4  42481  aks5lem3a  42559  imacrhmcl  42884  mendval  43536  hoidmvlelem3  46955  hspmbllem2  46985  isasslaw  48552  zlmodzxzscm  48717  lcoop  48771  lincvalsng  48776  lincvalpr  48778  lincdifsn  48784  islininds  48806  lines  49091  discsubc  49423  cofu2a  49454  cofid2  49474  cofidf2  49479  imaf1co  49514  upciclem1  49525  upfval2  49536  upfval3  49537  isuplem  49538  oppcup3lem  49565  uptrlem1  49569  uptr2  49580  swapfcoa  49640  tposcurf2val  49660  fuco21  49695  fuco23  49700  fuco22natlem3  49703  fucoid  49707  fucocolem2  49713  fucocolem4  49715  oppfdiag  49775  oppcthinendcALT  49800  isinito2lem  49857  dfinito4  49860  mndtchom  49943  mndtcco  49944  mndtccatid  49946  2arwcat  49959  setc1onsubc  49961  lanfval  49972  ranfval  49973  lanpropd  49974  ranpropd  49975  lanup  50000  ranup  50001  lmdfval  50008  cmdfval  50009  lmdpropd  50016  cmdpropd  50017  concom  50022  coccom  50023  islmd  50024  iscmd  50025  cmddu  50027