Theorem oveq123d 7171

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

Syntax hints:   → wi 4   = wceq 1533  (class class class)co 7150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153

This theorem is referenced by:  csbov123  7192  prdsplusgfval  16741  prdsmulrfval  16743  prdsvscafval  16747  prdsdsval2  16751  xpsaddlem  16840  xpsvsca  16844  iscat  16937  iscatd  16938  iscatd2  16946  catcocl  16950  catass  16951  moni  17000  rcaninv  17058  subccocl  17109  isfunc  17128  funcco  17135  idfucl  17145  cofuval  17146  cofuval2  17151  cofucl  17152  funcres  17160  ressffth  17202  isnat  17211  nati  17219  fuccoval  17227  coaval  17322  catcisolem  17360  xpcco  17427  xpcco2  17431  1stfcl  17441  2ndfcl  17442  prfcl  17447  evlf2  17462  evlfcllem  17465  evlfcl  17466  curfval  17467  curf1  17469  curf12  17471  curf1cl  17472  curf2  17473  curf2val  17474  curf2cl  17475  curfcl  17476  uncfcurf  17483  hofval  17496  hof2fval  17499  hofcl  17503  yonedalem4a  17519  yonedalem3  17524  yonedainv  17525  isdlat  17797  issgrp  17896  ismndd  17927  grpsubfval  18141  grpsubfvalALT  18142  grpsubpropd  18198  imasgrp  18209  subgsub  18285  eqgfval  18322  dpjfval  19171  issrg  19251  isring  19295  isringd  19329  dvrfval  19428  isdrngd  19521  issrngd  19626  islmodd  19634  isassa  20082  isassad  20090  asclfval  20102  ressascl  20119  psrval  20136  coe1tm  20435  evl1varpw  20518  isphld  20792  phlssphl  20797  pjfval  20844  islindf  20950  scmatval  21107  mdetfval  21189  smadiadetr  21278  pmatcollpw2lem  21379  pm2mpval  21397  pm2mpghm  21418  chpmatfval  21432  cpmadugsumlemB  21476  xkohmeo  22417  xpsdsval  22985  prdsxmslem2  23133  nmfval  23192  nmpropd  23197  nmpropd2  23198  subgnm  23236  tngnm  23254  cph2di  23805  cphassr  23810  ipcau2  23831  tcphcphlem2  23833  rrxplusgvscavalb  23992  q1pval  24741  r1pval  24744  dvntaylp  24953  israg  26477  ttgval  26655  grpodivfval  28305  dipfval  28473  lnoval  28523  ressnm  30633  isslmd  30825  fedgmullem2  31021  qqhval  31210  sitgval  31585  rdgeqoa  34645  prdsbnd2  35067  isrngo  35169  lflset  36189  islfld  36192  ldualset  36255  cmtfvalN  36340  isoml  36368  ltrnfset  37247  trlfset  37290  docaffvalN  38251  diblss  38300  dihffval  38360  dihfval  38361  hvmapffval  38888  hvmapfval  38889  hgmapfval  39016  mendval  39776  hoidmvlelem3  42873  hspmbllem2  42903  isasslaw  44093  isrng  44141  lidlmsgrp  44191  lidlrng  44192  zlmodzxzscm  44399  lcoop  44460  lincvalsng  44465  lincvalpr  44467  lincdifsn  44473  islininds  44495  lines  44712