Theorem oveq123d 7432

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

Syntax hints:   → wi 4   = wceq 1567  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  csbov123  7455  prdsplusgfval  17527  prdsmulrfval  17529  prdsvscafval  17533  prdsdsval2  17537  xpsaddlem  17627  xpsvsca  17631  iscat  17728  iscatd  17729  iscatd2  17737  catcocl  17741  catass  17742  moni  17793  rcaninv  17851  subccocl  17902  isfunc  17921  funcco  17928  idfucl  17938  cofuval  17939  cofuval2  17944  cofucl  17945  funcres  17953  ressffth  17997  isnat  18007  nati  18015  fuccoval  18023  coaval  18125  catcisolem  18167  xpcco  18239  xpcco2  18243  1stfcl  18253  2ndfcl  18254  prfcl  18259  evlf2  18274  evlfcllem  18277  evlfcl  18278  curfval  18279  curf1  18281  curf12  18283  curf1cl  18284  curf2  18285  curf2val  18286  curf2cl  18287  curfcl  18288  uncfcurf  18295  hofval  18308  hof2fval  18311  hofcl  18315  yonedalem4a  18331  yonedalem3  18336  yonedainv  18337  isdlat  18578  issgrp  18778  issgrpd  18788  ismndd  18814  grpsubfval  19050  grpsubfvalALT  19051  grpsubpropd  19111  imasgrp  19122  subgsub  19205  eqgfval  19244  dpjfval  20127  isrng  20232  isrngd  20251  issrg  20270  isring  20319  isringd  20374  dvrfval  20484  isdrngd  20847  isdrngdOLD  20849  issrngd  20936  islmodd  20965  rnglidlmsgrp  21354  rnglidlrng  21355  rngqiprngimf1lem  21405  isphld  21773  phlssphl  21778  pjfval  21825  islindf  21931  isassa  21975  isassad  21984  asclfval  21997  ressascl  22015  psrval  22034  psdffval  22289  coe1tm  22403  evl1varpw  22490  evls1maplmhm  22506  scmatval  22630  mdetfval  22712  smadiadetr  22801  pmatcollpw2lem  22903  pm2mpval  22921  pm2mpghm  22942  chpmatfval  22956  cpmadugsumlemB  23000  xkohmeo  23941  xpsdsval  24507  prdsxmslem2  24655  nmfval  24714  nmpropd  24720  nmpropd2  24721  subgnm  24759  tngnm  24777  cph2di  25335  cphassr  25340  ipcau2  25362  tcphcphlem2  25364  rrxplusgvscavalb  25523  q1pval  26281  r1pval  26284  dvntaylp  26500  israg  28936  ttgval  29165  grpodivfval  30827  dipfval  30995  lnoval  31045  ressnm  33225  isslmd  33463  erlval  33519  rlocval  33520  idlinsubrg  33683  zringfrac  33789  vietalem  33914  fedgmullem2  33965  qqhval  34307  sitgval  34667  rdgeqoa  37904  prdsbnd2  38334  isrngo  38436  lflset  39723  islfld  39726  ldualset  39789  cmtfvalN  39874  isoml  39902  ltrnfset  40781  trlfset  40824  docaffvalN  41785  diblss  41834  dihffval  41894  dihfval  41895  hvmapffval  42422  hvmapfval  42423  hgmapfval  42550  isprimroot  42750  primrootsunit1  42754  aks6d1c1p4  42768  aks5lem3a  42846  imacrhmcl  43178  mendval  43798  hoidmvlelem3  47203  hspmbllem2  47233  isasslaw  48846  zlmodzxzscm  49022  lcoop  49076  lincvalsng  49081  lincvalpr  49083  lincdifsn  49089  islininds  49111  lines  49396  discsubc  49727  cofu2a  49758  cofid2  49778  cofidf2  49783  imaf1co  49818  upciclem1  49829  upfval2  49840  upfval3  49841  isuplem  49842  oppcup3lem  49869  uptrlem1  49873  uptr2  49884  swapfcoa  49944  tposcurf2val  49964  fuco21  49999  fuco23  50004  fuco22natlem3  50007  fucoid  50011  fucocolem2  50017  fucocolem4  50019  oppfdiag  50079  oppcthinendcALT  50104  isinito2lem  50161  dfinito4  50164  mndtchom  50247  mndtcco  50248  mndtccatid  50250  2arwcat  50263  setc1onsubc  50265  lanfval  50276  ranfval  50277  lanpropd  50278  ranpropd  50279  lanup  50304  ranup  50305  lmdfval  50312  cmdfval  50313  lmdpropd  50320  cmdpropd  50321  concom  50326  coccom  50327  islmd  50328  iscmd  50329  cmddu  50331