Theorem oveq123d 7156

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

Syntax hints:   → wi 4   = wceq 1538  (class class class)co 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  csbov123  7177  prdsplusgfval  16739  prdsmulrfval  16741  prdsvscafval  16745  prdsdsval2  16749  xpsaddlem  16838  xpsvsca  16842  iscat  16935  iscatd  16936  iscatd2  16944  catcocl  16948  catass  16949  moni  16998  rcaninv  17056  subccocl  17107  isfunc  17126  funcco  17133  idfucl  17143  cofuval  17144  cofuval2  17149  cofucl  17150  funcres  17158  ressffth  17200  isnat  17209  nati  17217  fuccoval  17225  coaval  17320  catcisolem  17358  xpcco  17425  xpcco2  17429  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlf2  17460  evlfcllem  17463  evlfcl  17464  curfval  17465  curf1  17467  curf12  17469  curf1cl  17470  curf2  17471  curf2val  17472  curf2cl  17473  curfcl  17474  uncfcurf  17481  hofval  17494  hof2fval  17497  hofcl  17501  yonedalem4a  17517  yonedalem3  17522  yonedainv  17523  isdlat  17795  issgrp  17894  ismndd  17925  grpsubfval  18139  grpsubfvalALT  18140  grpsubpropd  18196  imasgrp  18207  subgsub  18283  eqgfval  18320  dpjfval  19170  issrg  19250  isring  19294  isringd  19331  dvrfval  19430  isdrngd  19520  issrngd  19625  islmodd  19633  isphld  20343  phlssphl  20348  pjfval  20395  islindf  20501  isassa  20545  isassad  20553  asclfval  20565  ressascl  20582  psrval  20600  coe1tm  20902  evl1varpw  20985  scmatval  21109  mdetfval  21191  smadiadetr  21280  pmatcollpw2lem  21382  pm2mpval  21400  pm2mpghm  21421  chpmatfval  21435  cpmadugsumlemB  21479  xkohmeo  22420  xpsdsval  22988  prdsxmslem2  23136  nmfval  23195  nmpropd  23200  nmpropd2  23201  subgnm  23239  tngnm  23257  cph2di  23812  cphassr  23817  ipcau2  23838  tcphcphlem2  23840  rrxplusgvscavalb  23999  q1pval  24754  r1pval  24757  dvntaylp  24966  israg  26491  ttgval  26669  grpodivfval  28317  dipfval  28485  lnoval  28535  ressnm  30664  isslmd  30880  idlinsubrg  31016  fedgmullem2  31114  qqhval  31325  sitgval  31700  rdgeqoa  34787  prdsbnd2  35233  isrngo  35335  lflset  36355  islfld  36358  ldualset  36421  cmtfvalN  36506  isoml  36534  ltrnfset  37413  trlfset  37456  docaffvalN  38417  diblss  38466  dihffval  38526  dihfval  38527  hvmapffval  39054  hvmapfval  39055  hgmapfval  39182  mendval  40127  hoidmvlelem3  43236  hspmbllem2  43266  isasslaw  44452  isrng  44500  lidlmsgrp  44550  lidlrng  44551  zlmodzxzscm  44759  lcoop  44820  lincvalsng  44825  lincvalpr  44827  lincdifsn  44833  islininds  44855  lines  45145