Theorem oveq123d 6826

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

Syntax hints:   → wi 4   = wceq 1624  (class class class)co 6805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808

This theorem is referenced by:  csbov123  6842  prdsplusgfval  16328  prdsmulrfval  16330  prdsvscafval  16334  prdsdsval2  16338  xpsaddlem  16429  xpsvsca  16433  iscat  16526  iscatd  16527  iscatd2  16535  catcocl  16539  catass  16540  moni  16589  rcaninv  16647  subccocl  16698  isfunc  16717  funcco  16724  idfucl  16734  cofuval  16735  cofuval2  16740  cofucl  16741  funcres  16749  ressffth  16791  isnat  16800  nati  16808  fuccoval  16816  coaval  16911  catcisolem  16949  xpcco  17016  xpcco2  17020  1stfcl  17030  2ndfcl  17031  prfcl  17036  evlf2  17051  evlfcllem  17054  evlfcl  17055  curfval  17056  curf1  17058  curf12  17060  curf1cl  17061  curf2  17062  curf2val  17063  curf2cl  17064  curfcl  17065  uncfcurf  17072  hofval  17085  hof2fval  17088  hofcl  17092  yonedalem4a  17108  yonedalem3  17113  yonedainv  17114  isdlat  17386  issgrp  17478  ismndd  17506  grpsubfval  17657  grpsubpropd  17713  imasgrp  17724  subgsub  17799  eqgfval  17835  dpjfval  18646  issrg  18699  isring  18743  isringd  18777  dvrfval  18876  isdrngd  18966  issrngd  19055  islmodd  19063  isassa  19509  isassad  19517  asclfval  19528  ressascl  19538  psrval  19556  coe1tm  19837  evl1varpw  19919  isphld  20193  pjfval  20244  islindf  20345  scmatval  20504  mdetfval  20586  smadiadetr  20675  pmatcollpw2lem  20776  pm2mpval  20794  pm2mpghm  20815  chpmatfval  20829  cpmadugsumlemB  20873  xkohmeo  21812  xpsdsval  22379  prdsxmslem2  22527  nmfval  22586  nmpropd  22591  nmpropd2  22592  subgnm  22630  tngnm  22648  cph2di  23199  cphassr  23204  ipcau2  23225  tchcphlem2  23227  q1pval  24104  r1pval  24107  dvntaylp  24316  israg  25783  ttgval  25946  grpodivfval  27689  dipfval  27858  lnoval  27908  ressnm  29952  isslmd  30056  qqhval  30319  sitgval  30695  rdgeqoa  33521  prdsbnd2  33899  isrngo  34001  lflset  34841  islfld  34844  ldualset  34907  cmtfvalN  34992  isoml  35020  ltrnfset  35898  trlfset  35942  docaffvalN  36904  diblss  36953  dihffval  37013  dihfval  37014  hvmapffval  37541  hvmapfval  37542  hgmapfval  37672  mendval  38247  hoidmvlelem3  41309  hspmbllem2  41339  isasslaw  42330  isrng  42378  lidlmsgrp  42428  lidlrng  42429  zlmodzxzscm  42637  lcoop  42702  lincvalsng  42707  lincvalpr  42709  lincdifsn  42715  islininds  42737