Theorem oveq123d 7424

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  csbov123  7447  prdsplusgfval  17486  prdsmulrfval  17488  prdsvscafval  17492  prdsdsval2  17496  xpsaddlem  17585  xpsvsca  17589  iscat  17682  iscatd  17683  iscatd2  17691  catcocl  17695  catass  17696  moni  17747  rcaninv  17805  subccocl  17856  isfunc  17875  funcco  17882  idfucl  17892  cofuval  17893  cofuval2  17898  cofucl  17899  funcres  17907  ressffth  17951  isnat  17961  nati  17969  fuccoval  17977  coaval  18079  catcisolem  18121  xpcco  18193  xpcco2  18197  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlf2  18228  evlfcllem  18231  evlfcl  18232  curfval  18233  curf1  18235  curf12  18237  curf1cl  18238  curf2  18239  curf2val  18240  curf2cl  18241  curfcl  18242  uncfcurf  18249  hofval  18262  hof2fval  18265  hofcl  18269  yonedalem4a  18285  yonedalem3  18290  yonedainv  18291  isdlat  18530  issgrp  18696  issgrpd  18706  ismndd  18732  grpsubfval  18964  grpsubfvalALT  18965  grpsubpropd  19026  imasgrp  19037  subgsub  19119  eqgfval  19157  dpjfval  20036  isrng  20112  isrngd  20131  issrg  20146  isring  20195  isringd  20249  dvrfval  20360  isdrngd  20723  isdrngdOLD  20725  issrngd  20813  islmodd  20821  rnglidlmsgrp  21205  rnglidlrng  21206  rngqiprngimf1lem  21253  isphld  21612  phlssphl  21617  pjfval  21664  islindf  21770  isassa  21814  isassad  21823  asclfval  21837  ressascl  21854  psrval  21873  psdffval  22093  coe1tm  22208  evl1varpw  22297  evls1maplmhm  22313  scmatval  22440  mdetfval  22522  smadiadetr  22611  pmatcollpw2lem  22713  pm2mpval  22731  pm2mpghm  22752  chpmatfval  22766  cpmadugsumlemB  22810  xkohmeo  23751  xpsdsval  24318  prdsxmslem2  24466  nmfval  24525  nmpropd  24531  nmpropd2  24532  subgnm  24570  tngnm  24588  cph2di  25157  cphassr  25162  ipcau2  25184  tcphcphlem2  25186  rrxplusgvscavalb  25345  q1pval  26110  r1pval  26113  dvntaylp  26329  israg  28622  ttgval  28800  grpodivfval  30461  dipfval  30629  lnoval  30679  ressnm  32886  isslmd  33145  erlval  33199  rlocval  33200  idlinsubrg  33392  zringfrac  33515  fedgmullem2  33616  qqhval  33949  sitgval  34310  rdgeqoa  37334  prdsbnd2  37765  isrngo  37867  lflset  39023  islfld  39026  ldualset  39089  cmtfvalN  39174  isoml  39202  ltrnfset  40082  trlfset  40125  docaffvalN  41086  diblss  41135  dihffval  41195  dihfval  41196  hvmapffval  41723  hvmapfval  41724  hgmapfval  41851  isprimroot  42052  primrootsunit1  42056  aks6d1c1p4  42070  aks5lem3a  42148  imacrhmcl  42484  mendval  43150  hoidmvlelem3  46574  hspmbllem2  46604  isasslaw  48115  zlmodzxzscm  48280  lcoop  48335  lincvalsng  48340  lincvalpr  48342  lincdifsn  48348  islininds  48370  lines  48659  discsubc  48979  imaf1co  49043  upciclem1  49049  upfval2  49060  upfval3  49061  isuplem  49062  oppcup3lem  49087  swapfcoa  49146  tposcurf2val  49160  fuco21  49195  fuco23  49200  fuco22natlem3  49203  fucoid  49207  fucocolem2  49213  fucocolem4  49215  oppcthinendcALT  49275  isinito2lem  49331  dfinito4  49334  mndtchom  49409  mndtcco  49410  mndtccatid  49412  2arwcat  49425  setc1onsubc  49427  lanfval  49438  ranfval  49439  lanup  49463  ranup  49464  lmdfval  49471  cmdfval  49472  concom  49481  coccom  49482  islmd  49483  iscmd  49484