Theorem oveq123d 7390

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  csbov123  7413  prdsplusgfval  17413  prdsmulrfval  17415  prdsvscafval  17419  prdsdsval2  17423  xpsaddlem  17512  xpsvsca  17516  iscat  17613  iscatd  17614  iscatd2  17622  catcocl  17626  catass  17627  moni  17678  rcaninv  17736  subccocl  17787  isfunc  17806  funcco  17813  idfucl  17823  cofuval  17824  cofuval2  17829  cofucl  17830  funcres  17838  ressffth  17882  isnat  17892  nati  17900  fuccoval  17908  coaval  18010  catcisolem  18052  xpcco  18124  xpcco2  18128  1stfcl  18138  2ndfcl  18139  prfcl  18144  evlf2  18159  evlfcllem  18162  evlfcl  18163  curfval  18164  curf1  18166  curf12  18168  curf1cl  18169  curf2  18170  curf2val  18171  curf2cl  18172  curfcl  18173  uncfcurf  18180  hofval  18193  hof2fval  18196  hofcl  18200  yonedalem4a  18216  yonedalem3  18221  yonedainv  18222  isdlat  18463  issgrp  18629  issgrpd  18639  ismndd  18665  grpsubfval  18897  grpsubfvalALT  18898  grpsubpropd  18959  imasgrp  18970  subgsub  19052  eqgfval  19090  dpjfval  19971  isrng  20074  isrngd  20093  issrg  20108  isring  20157  isringd  20211  dvrfval  20322  isdrngd  20685  isdrngdOLD  20687  issrngd  20775  islmodd  20804  rnglidlmsgrp  21188  rnglidlrng  21189  rngqiprngimf1lem  21236  isphld  21596  phlssphl  21601  pjfval  21648  islindf  21754  isassa  21798  isassad  21807  asclfval  21821  ressascl  21838  psrval  21857  psdffval  22077  coe1tm  22192  evl1varpw  22281  evls1maplmhm  22297  scmatval  22424  mdetfval  22506  smadiadetr  22595  pmatcollpw2lem  22697  pm2mpval  22715  pm2mpghm  22736  chpmatfval  22750  cpmadugsumlemB  22794  xkohmeo  23735  xpsdsval  24302  prdsxmslem2  24450  nmfval  24509  nmpropd  24515  nmpropd2  24516  subgnm  24554  tngnm  24572  cph2di  25140  cphassr  25145  ipcau2  25167  tcphcphlem2  25169  rrxplusgvscavalb  25328  q1pval  26093  r1pval  26096  dvntaylp  26312  israg  28677  ttgval  28855  grpodivfval  30513  dipfval  30681  lnoval  30731  ressnm  32936  isslmd  33171  erlval  33225  rlocval  33226  idlinsubrg  33395  zringfrac  33518  fedgmullem2  33619  qqhval  33955  sitgval  34316  rdgeqoa  37351  prdsbnd2  37782  isrngo  37884  lflset  39045  islfld  39048  ldualset  39111  cmtfvalN  39196  isoml  39224  ltrnfset  40104  trlfset  40147  docaffvalN  41108  diblss  41157  dihffval  41217  dihfval  41218  hvmapffval  41745  hvmapfval  41746  hgmapfval  41873  isprimroot  42074  primrootsunit1  42078  aks6d1c1p4  42092  aks5lem3a  42170  imacrhmcl  42495  mendval  43161  hoidmvlelem3  46588  hspmbllem2  46618  isasslaw  48173  zlmodzxzscm  48338  lcoop  48393  lincvalsng  48398  lincvalpr  48400  lincdifsn  48406  islininds  48428  lines  48713  discsubc  49046  cofu2a  49077  cofid2  49097  cofidf2  49102  imaf1co  49137  upciclem1  49148  upfval2  49159  upfval3  49160  isuplem  49161  oppcup3lem  49188  uptrlem1  49192  uptr2  49203  swapfcoa  49263  tposcurf2val  49283  fuco21  49318  fuco23  49323  fuco22natlem3  49326  fucoid  49330  fucocolem2  49336  fucocolem4  49338  oppfdiag  49398  oppcthinendcALT  49423  isinito2lem  49480  dfinito4  49483  mndtchom  49566  mndtcco  49567  mndtccatid  49569  2arwcat  49582  setc1onsubc  49584  lanfval  49595  ranfval  49596  lanpropd  49597  ranpropd  49598  lanup  49623  ranup  49624  lmdfval  49631  cmdfval  49632  lmdpropd  49639  cmdpropd  49640  concom  49645  coccom  49646  islmd  49647  iscmd  49648  cmddu  49650