Theorem oveq123d 7431

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

Syntax hints:   → wi 4   = wceq 1570  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  csbov123  7454  prdsplusgfval  17522  prdsmulrfval  17524  prdsvscafval  17528  prdsdsval2  17532  xpsaddlem  17622  xpsvsca  17626  iscat  17723  iscatd  17724  iscatd2  17732  catcocl  17736  catass  17737  moni  17788  rcaninv  17846  subccocl  17897  isfunc  17916  funcco  17923  idfucl  17933  cofuval  17934  cofuval2  17939  cofucl  17940  funcres  17948  ressffth  17992  isnat  18002  nati  18010  fuccoval  18018  coaval  18120  catcisolem  18162  xpcco  18234  xpcco2  18238  1stfcl  18248  2ndfcl  18249  prfcl  18254  evlf2  18269  evlfcllem  18272  evlfcl  18273  curfval  18274  curf1  18276  curf12  18278  curf1cl  18279  curf2  18280  curf2val  18281  curf2cl  18282  curfcl  18283  uncfcurf  18290  hofval  18303  hof2fval  18306  hofcl  18310  yonedalem4a  18326  yonedalem3  18331  yonedainv  18332  isdlat  18573  issgrp  18773  issgrpd  18783  ismndd  18809  grpsubfval  19045  grpsubfvalALT  19046  grpsubpropd  19106  imasgrp  19117  subgsub  19200  eqgfval  19239  dpjfval  20122  isrng  20227  isrngd  20246  issrg  20265  isring  20314  isringd  20370  dvrfval  20480  isdrngd  20868  isdrngdOLD  20870  issrngd  20958  islmodd  20987  rnglidlmsgrp  21380  rnglidlrng  21381  rngqiprngimf1lem  21434  isphld  21804  phlssphl  21809  pjfval  21856  islindf  21962  isassa  22006  isassad  22015  asclfval  22028  ressascl  22046  psrval  22065  psdffval  22320  coe1tm  22434  evl1varpw  22521  evls1maplmhm  22537  scmatval  22661  mdetfval  22743  smadiadetr  22832  pmatcollpw2lem  22934  pm2mpval  22952  pm2mpghm  22973  chpmatfval  22987  cpmadugsumlemB  23031  xkohmeo  23972  xpsdsval  24538  prdsxmslem2  24686  nmfval  24745  nmpropd  24751  nmpropd2  24752  subgnm  24790  tngnm  24808  cph2di  25366  cphassr  25371  ipcau2  25393  tcphcphlem2  25395  rrxplusgvscavalb  25554  q1pval  26312  r1pval  26315  dvntaylp  26534  israg  28977  ttgval  29224  grpodivfval  30886  dipfval  31054  lnoval  31104  ressnm  33284  isslmd  33522  erlval  33578  rlocval  33579  idlinsubrg  33739  zringfrac  33844  vietalem  33969  fedgmullem2  34020  qqhval  34362  sitgval  34722  rdgeqoa  38036  prdsbnd2  38466  isrngo  38568  lflset  39853  islfld  39856  ldualset  39919  cmtfvalN  40004  isoml  40032  ltrnfset  40911  trlfset  40954  docaffvalN  41915  diblss  41964  dihffval  42024  dihfval  42025  hvmapffval  42552  hvmapfval  42553  hgmapfval  42680  isprimroot  42880  primrootsunit1  42884  aks6d1c1p4  42898  aks5lem3a  42976  imacrhmcl  43308  mendval  43926  hoidmvlelem3  47331  hspmbllem2  47361  isasslaw  48977  zlmodzxzscm  49157  lcoop  49211  lincvalsng  49216  lincvalpr  49218  lincdifsn  49224  islininds  49246  lines  49531  discsubc  49862  cofu2a  49893  cofid2  49913  cofidf2  49918  imaf1co  49953  upciclem1  49964  upfval2  49975  upfval3  49976  isuplem  49977  oppcup3lem  50004  uptrlem1  50008  uptr2  50019  swapfcoa  50079  tposcurf2val  50099  fuco21  50134  fuco23  50139  fuco22natlem3  50142  fucoid  50146  fucocolem2  50152  fucocolem4  50154  oppfdiag  50214  oppcthinendcALT  50239  isinito2lem  50296  dfinito4  50299  mndtchom  50382  mndtcco  50383  mndtccatid  50385  2arwcat  50398  setc1onsubc  50400  lanfval  50411  ranfval  50412  lanpropd  50413  ranpropd  50414  lanup  50439  ranup  50440  lmdfval  50447  cmdfval  50448  lmdpropd  50455  cmdpropd  50456  concom  50461  coccom  50462  islmd  50463  iscmd  50464  cmddu  50466