Theorem oveq123d 7276

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

Syntax hints:   → wi 4   = wceq 1539  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  csbov123  7297  prdsplusgfval  17102  prdsmulrfval  17104  prdsvscafval  17108  prdsdsval2  17112  xpsaddlem  17201  xpsvsca  17205  iscat  17298  iscatd  17299  iscatd2  17307  catcocl  17311  catass  17312  moni  17365  rcaninv  17423  subccocl  17476  isfunc  17495  funcco  17502  idfucl  17512  cofuval  17513  cofuval2  17518  cofucl  17519  funcres  17527  ressffth  17570  isnat  17579  nati  17587  fuccoval  17597  coaval  17699  catcisolem  17741  xpcco  17816  xpcco2  17820  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlf2  17852  evlfcllem  17855  evlfcl  17856  curfval  17857  curf1  17859  curf12  17861  curf1cl  17862  curf2  17863  curf2val  17864  curf2cl  17865  curfcl  17866  uncfcurf  17873  hofval  17886  hof2fval  17889  hofcl  17893  yonedalem4a  17909  yonedalem3  17914  yonedainv  17915  isdlat  18155  issgrp  18291  ismndd  18322  grpsubfval  18538  grpsubfvalALT  18539  grpsubpropd  18595  imasgrp  18606  subgsub  18682  eqgfval  18719  dpjfval  19573  issrg  19658  isring  19702  isringd  19739  dvrfval  19841  isdrngd  19931  issrngd  20036  islmodd  20044  isphld  20771  phlssphl  20776  pjfval  20823  islindf  20929  isassa  20973  isassad  20981  asclfval  20993  ressascl  21010  psrval  21028  coe1tm  21354  evl1varpw  21437  scmatval  21561  mdetfval  21643  smadiadetr  21732  pmatcollpw2lem  21834  pm2mpval  21852  pm2mpghm  21873  chpmatfval  21887  cpmadugsumlemB  21931  xkohmeo  22874  xpsdsval  23442  prdsxmslem2  23591  nmfval  23650  nmpropd  23656  nmpropd2  23657  subgnm  23695  tngnm  23721  cph2di  24276  cphassr  24281  ipcau2  24303  tcphcphlem2  24305  rrxplusgvscavalb  24464  q1pval  25223  r1pval  25226  dvntaylp  25435  israg  26962  ttgval  27140  grpodivfval  28797  dipfval  28965  lnoval  29015  ressnm  31138  isslmd  31357  idlinsubrg  31510  fedgmullem2  31613  qqhval  31824  sitgval  32199  rdgeqoa  35468  prdsbnd2  35880  isrngo  35982  lflset  37000  islfld  37003  ldualset  37066  cmtfvalN  37151  isoml  37179  ltrnfset  38058  trlfset  38101  docaffvalN  39062  diblss  39111  dihffval  39171  dihfval  39172  hvmapffval  39699  hvmapfval  39700  hgmapfval  39827  mendval  40924  hoidmvlelem3  44025  hspmbllem2  44055  isasslaw  45274  isrng  45322  lidlmsgrp  45372  lidlrng  45373  zlmodzxzscm  45581  lcoop  45640  lincvalsng  45645  lincvalpr  45647  lincdifsn  45653  islininds  45675  lines  45965  mndtchom  46257  mndtcco  46258  mndtccatid  46260