Theorem oveq123d 7411

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  csbov123  7434  prdsplusgfval  17444  prdsmulrfval  17446  prdsvscafval  17450  prdsdsval2  17454  xpsaddlem  17543  xpsvsca  17547  iscat  17640  iscatd  17641  iscatd2  17649  catcocl  17653  catass  17654  moni  17705  rcaninv  17763  subccocl  17814  isfunc  17833  funcco  17840  idfucl  17850  cofuval  17851  cofuval2  17856  cofucl  17857  funcres  17865  ressffth  17909  isnat  17919  nati  17927  fuccoval  17935  coaval  18037  catcisolem  18079  xpcco  18151  xpcco2  18155  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlf2  18186  evlfcllem  18189  evlfcl  18190  curfval  18191  curf1  18193  curf12  18195  curf1cl  18196  curf2  18197  curf2val  18198  curf2cl  18199  curfcl  18200  uncfcurf  18207  hofval  18220  hof2fval  18223  hofcl  18227  yonedalem4a  18243  yonedalem3  18248  yonedainv  18249  isdlat  18488  issgrp  18654  issgrpd  18664  ismndd  18690  grpsubfval  18922  grpsubfvalALT  18923  grpsubpropd  18984  imasgrp  18995  subgsub  19077  eqgfval  19115  dpjfval  19994  isrng  20070  isrngd  20089  issrg  20104  isring  20153  isringd  20207  dvrfval  20318  isdrngd  20681  isdrngdOLD  20683  issrngd  20771  islmodd  20779  rnglidlmsgrp  21163  rnglidlrng  21164  rngqiprngimf1lem  21211  isphld  21570  phlssphl  21575  pjfval  21622  islindf  21728  isassa  21772  isassad  21781  asclfval  21795  ressascl  21812  psrval  21831  psdffval  22051  coe1tm  22166  evl1varpw  22255  evls1maplmhm  22271  scmatval  22398  mdetfval  22480  smadiadetr  22569  pmatcollpw2lem  22671  pm2mpval  22689  pm2mpghm  22710  chpmatfval  22724  cpmadugsumlemB  22768  xkohmeo  23709  xpsdsval  24276  prdsxmslem2  24424  nmfval  24483  nmpropd  24489  nmpropd2  24490  subgnm  24528  tngnm  24546  cph2di  25114  cphassr  25119  ipcau2  25141  tcphcphlem2  25143  rrxplusgvscavalb  25302  q1pval  26067  r1pval  26070  dvntaylp  26286  israg  28631  ttgval  28809  grpodivfval  30470  dipfval  30638  lnoval  30688  ressnm  32893  isslmd  33162  erlval  33216  rlocval  33217  idlinsubrg  33409  zringfrac  33532  fedgmullem2  33633  qqhval  33969  sitgval  34330  rdgeqoa  37365  prdsbnd2  37796  isrngo  37898  lflset  39059  islfld  39062  ldualset  39125  cmtfvalN  39210  isoml  39238  ltrnfset  40118  trlfset  40161  docaffvalN  41122  diblss  41171  dihffval  41231  dihfval  41232  hvmapffval  41759  hvmapfval  41760  hgmapfval  41887  isprimroot  42088  primrootsunit1  42092  aks6d1c1p4  42106  aks5lem3a  42184  imacrhmcl  42509  mendval  43175  hoidmvlelem3  46602  hspmbllem2  46632  isasslaw  48184  zlmodzxzscm  48349  lcoop  48404  lincvalsng  48409  lincvalpr  48411  lincdifsn  48417  islininds  48439  lines  48724  discsubc  49057  cofu2a  49088  cofid2  49108  cofidf2  49113  imaf1co  49148  upciclem1  49159  upfval2  49170  upfval3  49171  isuplem  49172  oppcup3lem  49199  uptrlem1  49203  uptr2  49214  swapfcoa  49274  tposcurf2val  49294  fuco21  49329  fuco23  49334  fuco22natlem3  49337  fucoid  49341  fucocolem2  49347  fucocolem4  49349  oppfdiag  49409  oppcthinendcALT  49434  isinito2lem  49491  dfinito4  49494  mndtchom  49577  mndtcco  49578  mndtccatid  49580  2arwcat  49593  setc1onsubc  49595  lanfval  49606  ranfval  49607  lanpropd  49608  ranpropd  49609  lanup  49634  ranup  49635  lmdfval  49642  cmdfval  49643  lmdpropd  49650  cmdpropd  49651  concom  49656  coccom  49657  islmd  49658  iscmd  49659  cmddu  49661