Theorem oveq123d 7377

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

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  csbov123  7400  prdsplusgfval  17392  prdsmulrfval  17394  prdsvscafval  17398  prdsdsval2  17402  xpsaddlem  17492  xpsvsca  17496  iscat  17593  iscatd  17594  iscatd2  17602  catcocl  17606  catass  17607  moni  17658  rcaninv  17716  subccocl  17767  isfunc  17786  funcco  17793  idfucl  17803  cofuval  17804  cofuval2  17809  cofucl  17810  funcres  17818  ressffth  17862  isnat  17872  nati  17880  fuccoval  17888  coaval  17990  catcisolem  18032  xpcco  18104  xpcco2  18108  1stfcl  18118  2ndfcl  18119  prfcl  18124  evlf2  18139  evlfcllem  18142  evlfcl  18143  curfval  18144  curf1  18146  curf12  18148  curf1cl  18149  curf2  18150  curf2val  18151  curf2cl  18152  curfcl  18153  uncfcurf  18160  hofval  18173  hof2fval  18176  hofcl  18180  yonedalem4a  18196  yonedalem3  18201  yonedainv  18202  isdlat  18443  issgrp  18643  issgrpd  18653  ismndd  18679  grpsubfval  18911  grpsubfvalALT  18912  grpsubpropd  18973  imasgrp  18984  subgsub  19066  eqgfval  19103  dpjfval  19984  isrng  20087  isrngd  20106  issrg  20121  isring  20170  isringd  20224  dvrfval  20336  isdrngd  20696  isdrngdOLD  20698  issrngd  20786  islmodd  20815  rnglidlmsgrp  21199  rnglidlrng  21200  rngqiprngimf1lem  21247  isphld  21607  phlssphl  21612  pjfval  21659  islindf  21765  isassa  21809  isassad  21818  asclfval  21832  ressascl  21850  psrval  21869  psdffval  22098  coe1tm  22213  evl1varpw  22303  evls1maplmhm  22319  scmatval  22446  mdetfval  22528  smadiadetr  22617  pmatcollpw2lem  22719  pm2mpval  22737  pm2mpghm  22758  chpmatfval  22772  cpmadugsumlemB  22816  xkohmeo  23757  xpsdsval  24323  prdsxmslem2  24471  nmfval  24530  nmpropd  24536  nmpropd2  24537  subgnm  24575  tngnm  24593  cph2di  25161  cphassr  25166  ipcau2  25188  tcphcphlem2  25190  rrxplusgvscavalb  25349  q1pval  26114  r1pval  26117  dvntaylp  26333  israg  28718  ttgval  28896  grpodivfval  30558  dipfval  30726  lnoval  30776  ressnm  32995  isslmd  33233  erlval  33289  rlocval  33290  idlinsubrg  33461  zringfrac  33584  vietalem  33684  fedgmullem2  33736  qqhval  34078  sitgval  34438  rdgeqoa  37514  prdsbnd2  37935  isrngo  38037  lflset  39258  islfld  39261  ldualset  39324  cmtfvalN  39409  isoml  39437  ltrnfset  40316  trlfset  40359  docaffvalN  41320  diblss  41369  dihffval  41429  dihfval  41430  hvmapffval  41957  hvmapfval  41958  hgmapfval  42085  isprimroot  42286  primrootsunit1  42290  aks6d1c1p4  42304  aks5lem3a  42382  imacrhmcl  42711  mendval  43363  hoidmvlelem3  46783  hspmbllem2  46813  isasslaw  48380  zlmodzxzscm  48545  lcoop  48599  lincvalsng  48604  lincvalpr  48606  lincdifsn  48612  islininds  48634  lines  48919  discsubc  49251  cofu2a  49282  cofid2  49302  cofidf2  49307  imaf1co  49342  upciclem1  49353  upfval2  49364  upfval3  49365  isuplem  49366  oppcup3lem  49393  uptrlem1  49397  uptr2  49408  swapfcoa  49468  tposcurf2val  49488  fuco21  49523  fuco23  49528  fuco22natlem3  49531  fucoid  49535  fucocolem2  49541  fucocolem4  49543  oppfdiag  49603  oppcthinendcALT  49628  isinito2lem  49685  dfinito4  49688  mndtchom  49771  mndtcco  49772  mndtccatid  49774  2arwcat  49787  setc1onsubc  49789  lanfval  49800  ranfval  49801  lanpropd  49802  ranpropd  49803  lanup  49828  ranup  49829  lmdfval  49836  cmdfval  49837  lmdpropd  49844  cmdpropd  49845  concom  49850  coccom  49851  islmd  49852  iscmd  49853  cmddu  49855