MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq123d Structured version   Unicode version

Theorem oveq123d 6291
Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
oveq123d.1  |-  ( ph  ->  F  =  G )
oveq123d.2  |-  ( ph  ->  A  =  B )
oveq123d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
oveq123d  |-  ( ph  ->  ( A F C )  =  ( B G D ) )

Proof of Theorem oveq123d
StepHypRef Expression
1 oveq123d.1 . . 3  |-  ( ph  ->  F  =  G )
21oveqd 6287 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6288 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2495 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398  (class class class)co 6270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  csbov123  6304  prdsplusgfval  14966  prdsmulrfval  14968  prdsvscafval  14972  prdsdsval2  14976  xpsaddlem  15067  xpsvsca  15071  iscat  15164  iscatd  15165  iscatd2  15173  catcocl  15177  catass  15178  moni  15227  rcaninv  15285  subccocl  15336  isfunc  15355  funcco  15362  idfucl  15372  cofuval  15373  cofuval2  15378  cofucl  15379  funcres  15387  ressffth  15429  isnat  15438  nati  15446  fuccoval  15454  coaval  15549  catcisolem  15587  xpcco  15654  xpcco2  15658  1stfcl  15668  2ndfcl  15669  prfcl  15674  evlf2  15689  evlfcllem  15692  evlfcl  15693  curfval  15694  curf1  15696  curf12  15698  curf1cl  15699  curf2  15700  curf2val  15701  curf2cl  15702  curfcl  15703  uncfcurf  15710  hofval  15723  hof2fval  15726  hofcl  15730  yonedalem4a  15746  yonedalem3  15751  yonedainv  15752  isdlat  16025  issgrp  16114  ismndOLD  16128  ismndd  16145  grpsubfval  16294  grpsubpropd  16342  imasgrp  16388  subgsub  16415  eqgfval  16451  dpjfval  17302  issrg  17357  isring  17400  isringd  17431  dvrfval  17531  isdrngd  17619  issrngd  17708  islmodd  17716  isassa  18162  isassad  18170  asclfval  18181  ressascl  18191  psrval  18209  coe1tm  18512  evl1varpw  18595  isphld  18865  pjfval  18913  islindf  19017  scmatval  19176  mdetfval  19258  smadiadetr  19347  pmatcollpw2lem  19448  pm2mpval  19466  pm2mpghm  19487  chpmatfval  19501  cpmadugsumlemB  19545  xkohmeo  20485  xpsdsval  21053  prdsxmslem2  21201  nmfval  21278  nmpropd  21283  nmpropd2  21284  subgnm  21316  tngnm  21334  cph2di  21822  cphassr  21827  ipcau2  21846  tchcphlem2  21848  q1pval  22723  r1pval  22726  dvntaylp  22935  israg  24278  ttgval  24383  grpodivfval  25445  isrngo  25581  dipfval  25813  lnoval  25868  ressnm  27876  isslmd  27982  qqhval  28192  sitgval  28541  prdsbnd2  30534  mendval  31376  isasslaw  32907  isrng  32955  lidlmsgrp  33005  lidlrng  33006  zlmodzxzscm  33219  lcoop  33285  lincvalsng  33290  lincvalpr  33292  lincdifsn  33298  islininds  33320  lflset  35200  islfld  35203  ldualset  35266  cmtfvalN  35351  isoml  35379  ltrnfset  36257  trlfset  36301  docaffvalN  37264  diblss  37313  dihffval  37373  dihfval  37374  hvmapffval  37901  hvmapfval  37902  hgmapfval  38032
  Copyright terms: Public domain W3C validator