Theorem oveq123d 7469

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

Syntax hints:   → wi 4   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  csbov123  7492  prdsplusgfval  17534  prdsmulrfval  17536  prdsvscafval  17540  prdsdsval2  17544  xpsaddlem  17633  xpsvsca  17637  iscat  17730  iscatd  17731  iscatd2  17739  catcocl  17743  catass  17744  moni  17797  rcaninv  17855  subccocl  17909  isfunc  17928  funcco  17935  idfucl  17945  cofuval  17946  cofuval2  17951  cofucl  17952  funcres  17960  ressffth  18005  isnat  18015  nati  18023  fuccoval  18033  coaval  18135  catcisolem  18177  xpcco  18252  xpcco2  18256  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlf2  18288  evlfcllem  18291  evlfcl  18292  curfval  18293  curf1  18295  curf12  18297  curf1cl  18298  curf2  18299  curf2val  18300  curf2cl  18301  curfcl  18302  uncfcurf  18309  hofval  18322  hof2fval  18325  hofcl  18329  yonedalem4a  18345  yonedalem3  18350  yonedainv  18351  isdlat  18592  issgrp  18758  issgrpd  18768  ismndd  18794  grpsubfval  19023  grpsubfvalALT  19024  grpsubpropd  19085  imasgrp  19096  subgsub  19178  eqgfval  19216  dpjfval  20099  isrng  20181  isrngd  20200  issrg  20215  isring  20264  isringd  20314  dvrfval  20428  isdrngd  20787  isdrngdOLD  20789  issrngd  20878  islmodd  20886  rnglidlmsgrp  21279  rnglidlrng  21280  rngqiprngimf1lem  21327  isphld  21695  phlssphl  21700  pjfval  21749  islindf  21855  isassa  21899  isassad  21908  asclfval  21922  ressascl  21939  psrval  21958  psdffval  22184  coe1tm  22297  evl1varpw  22386  evls1maplmhm  22402  scmatval  22531  mdetfval  22613  smadiadetr  22702  pmatcollpw2lem  22804  pm2mpval  22822  pm2mpghm  22843  chpmatfval  22857  cpmadugsumlemB  22901  xkohmeo  23844  xpsdsval  24412  prdsxmslem2  24563  nmfval  24622  nmpropd  24628  nmpropd2  24629  subgnm  24667  tngnm  24693  cph2di  25260  cphassr  25265  ipcau2  25287  tcphcphlem2  25289  rrxplusgvscavalb  25448  q1pval  26214  r1pval  26217  dvntaylp  26431  israg  28723  ttgval  28901  ttgvalOLD  28902  grpodivfval  30566  dipfval  30734  lnoval  30784  ressnm  32931  isslmd  33181  erlval  33230  rlocval  33231  idlinsubrg  33424  zringfrac  33547  fedgmullem2  33643  qqhval  33920  sitgval  34297  rdgeqoa  37336  prdsbnd2  37755  isrngo  37857  lflset  39015  islfld  39018  ldualset  39081  cmtfvalN  39166  isoml  39194  ltrnfset  40074  trlfset  40117  docaffvalN  41078  diblss  41127  dihffval  41187  dihfval  41188  hvmapffval  41715  hvmapfval  41716  hgmapfval  41843  isprimroot  42050  primrootsunit1  42054  aks6d1c1p4  42068  aks5lem3a  42146  imacrhmcl  42469  mendval  43140  hoidmvlelem3  46518  hspmbllem2  46548  isasslaw  47915  zlmodzxzscm  48082  lcoop  48140  lincvalsng  48145  lincvalpr  48147  lincdifsn  48153  islininds  48175  lines  48465  mndtchom  48757  mndtcco  48758  mndtccatid  48760