Theorem oveq123d 7472

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  csbov123  7495  prdsplusgfval  17695  prdsmulrfval  17697  prdsvscafval  17701  prdsdsval2  17705  xpsaddlem  17795  xpsvsca  17799  iscat  17896  iscatd  17897  iscatd2  17905  catcocl  17909  catass  17910  moni  17961  rcaninv  18019  subccocl  18070  isfunc  18089  funcco  18096  idfucl  18106  cofuval  18107  cofuval2  18112  cofucl  18113  funcres  18121  ressffth  18165  isnat  18175  nati  18183  fuccoval  18191  coaval  18293  catcisolem  18335  xpcco  18407  xpcco2  18411  1stfcl  18421  2ndfcl  18422  prfcl  18427  evlf2  18442  evlfcllem  18445  evlfcl  18446  curfval  18447  curf1  18449  curf12  18451  curf1cl  18452  curf2  18453  curf2val  18454  curf2cl  18455  curfcl  18456  uncfcurf  18463  hofval  18476  hof2fval  18479  hofcl  18483  yonedalem4a  18499  yonedalem3  18504  yonedainv  18505  isdlat  18746  issgrp  18959  issgrpd  18969  ismndd  18996  grpsubfval  19244  grpsubfvalALT  19245  grpsubpropd  19305  imasgrp  19316  subgsub  19399  eqgfval  19438  dpjfval  20322  isrng  20427  isrngd  20446  issrg  20465  isring  20514  isringd  20573  dvrfval  20683  isdrngd  21073  isdrngdOLD  21075  issrngd  21163  islmodd  21192  rnglidlmsgrp  21585  rnglidlrng  21586  rngqiprngimf1lem  21641  isphld  22015  phlssphl  22020  pjfval  22067  islindf  22173  isassa  22219  isassad  22228  asclfval  22241  ressascl  22259  psrval  22278  psdffval  22533  coe1tm  22647  evl1varpw  22734  evls1maplmhm  22750  scmatval  22874  mdetfval  22956  smadiadetr  23045  pmatcollpw2lem  23150  pm2mpval  23168  pm2mpghm  23189  chpmatfval  23203  cpmadugsumlemB  23247  xkohmeo  24189  xpsdsval  24755  prdsxmslem2  24903  nmfval  24962  nmpropd  24968  nmpropd2  24969  subgnm  25007  tngnm  25025  cph2di  25583  cphassr  25588  ipcau2  25610  tcphcphlem2  25612  rrxplusgvscavalb  25771  q1pval  26528  r1pval  26531  dvntaylp  26755  israg  29229  ttgval  29509  grpodivfval  31193  dipfval  31361  lnoval  31411  ressnm  33621  isslmd  33862  erlval  33918  rlocval  33919  isedom  33953  idlinsubrg  34085  zringfrac  34189  vietalem  34322  fedgmullem2  34373  qqhval  34715  sitgval  35075  rdgeqoa  38561  prdsbnd2  38995  isrngo  39097  lflset  40382  islfld  40385  ldualset  40448  cmtfvalN  40533  isoml  40561  ltrnfset  41440  trlfset  41483  docaffvalN  42444  diblss  42493  dihffval  42553  dihfval  42554  hvmapffval  43081  hvmapfval  43082  hgmapfval  43209  isprimroot  43409  primrootsunit1  43413  aks6d1c1p4  43427  aks5lem3a  43505  imacrhmcl  43847  prjspnnorm  43927  mendval  44442  hoidmvlelem3  47880  hspmbllem2  47910  isasslaw  49562  zlmodzxzscm  49800  lcoop  49854  lincvalsng  49859  lincvalpr  49861  lincdifsn  49867  islininds  49889  lines  50175  discsubc  50509  cofu2a  50541  cofid2  50562  cofidf2  50567  imaf1co  50602  upciclem1  50613  upfval2  50624  upfval3  50625  isuplem  50626  oppcup3lem  50653  uptrlem1  50657  uptr2  50668  swapfcoa  50734  tposcurf2val  50754  fuco21  50789  fuco23  50794  fuco22natlem3  50797  fucoid  50801  fucocolem2  50807  fucocolem4  50809  oppfdiag  50882  oppcthinendcALT  50907  isinito2lem  50964  dfinito4  50967  mndtchom  51053  mndtcco  51054  mndtccatid  51056  2arwcat  51069  setc1onsubc  51071  parcoval2  51097  parmapfunc2  51105  parmapfunc  51106  lanfval  51127  ranfval  51128  lanpropd  51129  ranpropd  51130  lanup  51155  ranup  51156  lmdfval  51163  cmdfval  51164  lmdpropd  51171  cmdpropd  51172  concom  51177  coccom  51178  islmd  51179  iscmd  51180  cmddu  51182