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

Theorem oveq123d 6303
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 6299 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6300 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2508 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379  (class class class)co 6282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  csbov123  6313  csbovgOLD  6315  prdsplusgfval  14725  prdsmulrfval  14727  prdsvscafval  14731  prdsdsval2  14735  xpsaddlem  14826  xpsvsca  14830  iscat  14923  iscatd  14924  iscatd2  14932  catcocl  14936  catass  14937  moni  14988  subccocl  15068  isfunc  15087  funcco  15094  idfucl  15104  cofuval  15105  cofuval2  15110  cofucl  15111  funcres  15119  ressffth  15161  isnat  15170  nati  15178  fuccoval  15186  coaval  15249  catcisolem  15287  xpcco  15306  xpcco2  15310  1stfcl  15320  2ndfcl  15321  prfcl  15326  evlf2  15341  evlfcllem  15344  evlfcl  15345  curfval  15346  curf1  15348  curf12  15350  curf1cl  15351  curf2  15352  curf2val  15353  curf2cl  15354  curfcl  15355  uncfcurf  15362  hofval  15375  hof2fval  15378  hofcl  15382  yonedalem4a  15398  yonedalem3  15403  yonedainv  15404  isdlat  15676  ismnd  15730  ismndd  15757  grpsubfval  15893  grpsubpropd  15941  imasgrp  15986  subgsub  16008  eqgfval  16044  dpjfval  16894  issrg  16949  isrng  16990  isrngd  17020  dvrfval  17117  isdrngd  17204  issrngd  17293  islmodd  17301  isassa  17735  isassad  17743  asclfval  17754  ressascl  17764  psrval  17782  coe1tm  18085  evl1varpw  18168  isphld  18456  pjfval  18504  islindf  18614  scmatval  18773  mdetfval  18855  smadiadetr  18944  pmatcollpw2lem  19045  pm2mpval  19063  pm2mpghm  19084  chpmatfval  19098  cpmadugsumlemB  19142  xkohmeo  20051  xpsdsval  20619  prdsxmslem2  20767  nmfval  20844  nmpropd  20849  nmpropd2  20850  subgnm  20882  tngnm  20900  cph2di  21388  cphassr  21393  ipcau2  21412  tchcphlem2  21414  q1pval  22289  r1pval  22292  dvntaylp  22500  israg  23782  ttgval  23854  grpodivfval  24920  isrngo  25056  dipfval  25288  lnoval  25343  ressnm  27301  isslmd  27407  qqhval  27591  sitgval  27914  prdsbnd2  29894  mendval  30737  issgrp  31928  isasslaw  31941  isrng0  31981  zlmodzxzscm  32010  lcoop  32085  lincvalsng  32090  lincvalpr  32092  lincdifsn  32098  islininds  32120  lflset  33856  islfld  33859  ldualset  33922  cmtfvalN  34007  isoml  34035  ltrnfset  34913  trlfset  34956  docaffvalN  35918  diblss  35967  dihffval  36027  dihfval  36028  hvmapffval  36555  hvmapfval  36556  hgmapfval  36686
  Copyright terms: Public domain W3C validator