Theorem oveq123d 7408

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  csbov123  7431  prdsplusgfval  17437  prdsmulrfval  17439  prdsvscafval  17443  prdsdsval2  17447  xpsaddlem  17536  xpsvsca  17540  iscat  17633  iscatd  17634  iscatd2  17642  catcocl  17646  catass  17647  moni  17698  rcaninv  17756  subccocl  17807  isfunc  17826  funcco  17833  idfucl  17843  cofuval  17844  cofuval2  17849  cofucl  17850  funcres  17858  ressffth  17902  isnat  17912  nati  17920  fuccoval  17928  coaval  18030  catcisolem  18072  xpcco  18144  xpcco2  18148  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlf2  18179  evlfcllem  18182  evlfcl  18183  curfval  18184  curf1  18186  curf12  18188  curf1cl  18189  curf2  18190  curf2val  18191  curf2cl  18192  curfcl  18193  uncfcurf  18200  hofval  18213  hof2fval  18216  hofcl  18220  yonedalem4a  18236  yonedalem3  18241  yonedainv  18242  isdlat  18481  issgrp  18647  issgrpd  18657  ismndd  18683  grpsubfval  18915  grpsubfvalALT  18916  grpsubpropd  18977  imasgrp  18988  subgsub  19070  eqgfval  19108  dpjfval  19987  isrng  20063  isrngd  20082  issrg  20097  isring  20146  isringd  20200  dvrfval  20311  isdrngd  20674  isdrngdOLD  20676  issrngd  20764  islmodd  20772  rnglidlmsgrp  21156  rnglidlrng  21157  rngqiprngimf1lem  21204  isphld  21563  phlssphl  21568  pjfval  21615  islindf  21721  isassa  21765  isassad  21774  asclfval  21788  ressascl  21805  psrval  21824  psdffval  22044  coe1tm  22159  evl1varpw  22248  evls1maplmhm  22264  scmatval  22391  mdetfval  22473  smadiadetr  22562  pmatcollpw2lem  22664  pm2mpval  22682  pm2mpghm  22703  chpmatfval  22717  cpmadugsumlemB  22761  xkohmeo  23702  xpsdsval  24269  prdsxmslem2  24417  nmfval  24476  nmpropd  24482  nmpropd2  24483  subgnm  24521  tngnm  24539  cph2di  25107  cphassr  25112  ipcau2  25134  tcphcphlem2  25136  rrxplusgvscavalb  25295  q1pval  26060  r1pval  26063  dvntaylp  26279  israg  28624  ttgval  28802  grpodivfval  30463  dipfval  30631  lnoval  30681  ressnm  32886  isslmd  33155  erlval  33209  rlocval  33210  idlinsubrg  33402  zringfrac  33525  fedgmullem2  33626  qqhval  33962  sitgval  34323  rdgeqoa  37358  prdsbnd2  37789  isrngo  37891  lflset  39052  islfld  39055  ldualset  39118  cmtfvalN  39203  isoml  39231  ltrnfset  40111  trlfset  40154  docaffvalN  41115  diblss  41164  dihffval  41224  dihfval  41225  hvmapffval  41752  hvmapfval  41753  hgmapfval  41880  isprimroot  42081  primrootsunit1  42085  aks6d1c1p4  42099  aks5lem3a  42177  imacrhmcl  42502  mendval  43168  hoidmvlelem3  46595  hspmbllem2  46625  isasslaw  48180  zlmodzxzscm  48345  lcoop  48400  lincvalsng  48405  lincvalpr  48407  lincdifsn  48413  islininds  48435  lines  48720  discsubc  49053  cofu2a  49084  cofid2  49104  cofidf2  49109  imaf1co  49144  upciclem1  49155  upfval2  49166  upfval3  49167  isuplem  49168  oppcup3lem  49195  uptrlem1  49199  uptr2  49210  swapfcoa  49270  tposcurf2val  49290  fuco21  49325  fuco23  49330  fuco22natlem3  49333  fucoid  49337  fucocolem2  49343  fucocolem4  49345  oppfdiag  49405  oppcthinendcALT  49430  isinito2lem  49487  dfinito4  49490  mndtchom  49573  mndtcco  49574  mndtccatid  49576  2arwcat  49589  setc1onsubc  49591  lanfval  49602  ranfval  49603  lanpropd  49604  ranpropd  49605  lanup  49630  ranup  49631  lmdfval  49638  cmdfval  49639  lmdpropd  49646  cmdpropd  49647  concom  49652  coccom  49653  islmd  49654  iscmd  49655  cmddu  49657