Theorem oveq123d 7177

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

Syntax hints:   → wi 4   = wceq 1538  (class class class)co 7156

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-ov 7159

This theorem is referenced by:  csbov123  7198  prdsplusgfval  16818  prdsmulrfval  16820  prdsvscafval  16824  prdsdsval2  16828  xpsaddlem  16917  xpsvsca  16921  iscat  17014  iscatd  17015  iscatd2  17023  catcocl  17027  catass  17028  moni  17078  rcaninv  17136  subccocl  17187  isfunc  17206  funcco  17213  idfucl  17223  cofuval  17224  cofuval2  17229  cofucl  17230  funcres  17238  ressffth  17280  isnat  17289  nati  17297  fuccoval  17305  coaval  17407  catcisolem  17445  xpcco  17512  xpcco2  17516  1stfcl  17526  2ndfcl  17527  prfcl  17532  evlf2  17547  evlfcllem  17550  evlfcl  17551  curfval  17552  curf1  17554  curf12  17556  curf1cl  17557  curf2  17558  curf2val  17559  curf2cl  17560  curfcl  17561  uncfcurf  17568  hofval  17581  hof2fval  17584  hofcl  17588  yonedalem4a  17604  yonedalem3  17609  yonedainv  17610  isdlat  17882  issgrp  17981  ismndd  18012  grpsubfval  18227  grpsubfvalALT  18228  grpsubpropd  18284  imasgrp  18295  subgsub  18371  eqgfval  18408  dpjfval  19258  issrg  19338  isring  19382  isringd  19419  dvrfval  19518  isdrngd  19608  issrngd  19713  islmodd  19721  isphld  20432  phlssphl  20437  pjfval  20484  islindf  20590  isassa  20634  isassad  20642  asclfval  20654  ressascl  20672  psrval  20690  coe1tm  21010  evl1varpw  21093  scmatval  21217  mdetfval  21299  smadiadetr  21388  pmatcollpw2lem  21490  pm2mpval  21508  pm2mpghm  21529  chpmatfval  21543  cpmadugsumlemB  21587  xkohmeo  22528  xpsdsval  23096  prdsxmslem2  23244  nmfval  23303  nmpropd  23309  nmpropd2  23310  subgnm  23348  tngnm  23366  cph2di  23921  cphassr  23926  ipcau2  23947  tcphcphlem2  23949  rrxplusgvscavalb  24108  q1pval  24866  r1pval  24869  dvntaylp  25078  israg  26603  ttgval  26781  grpodivfval  28429  dipfval  28597  lnoval  28647  ressnm  30772  isslmd  30993  idlinsubrg  31141  fedgmullem2  31244  qqhval  31455  sitgval  31830  rdgeqoa  35101  prdsbnd2  35547  isrngo  35649  lflset  36669  islfld  36672  ldualset  36735  cmtfvalN  36820  isoml  36848  ltrnfset  37727  trlfset  37770  docaffvalN  38731  diblss  38780  dihffval  38840  dihfval  38841  hvmapffval  39368  hvmapfval  39369  hgmapfval  39496  mendval  40535  hoidmvlelem3  43637  hspmbllem2  43667  isasslaw  44868  isrng  44916  lidlmsgrp  44966  lidlrng  44967  zlmodzxzscm  45175  lcoop  45234  lincvalsng  45239  lincvalpr  45241  lincdifsn  45247  islininds  45269  lines  45559