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

Theorem oveq123d 6326
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 6322 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6323 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2470 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437  (class class class)co 6305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  csbov123  6339  prdsplusgfval  15331  prdsmulrfval  15333  prdsvscafval  15337  prdsdsval2  15341  xpsaddlem  15432  xpsvsca  15436  iscat  15529  iscatd  15530  iscatd2  15538  catcocl  15542  catass  15543  moni  15592  rcaninv  15650  subccocl  15701  isfunc  15720  funcco  15727  idfucl  15737  cofuval  15738  cofuval2  15743  cofucl  15744  funcres  15752  ressffth  15794  isnat  15803  nati  15811  fuccoval  15819  coaval  15914  catcisolem  15952  xpcco  16019  xpcco2  16023  1stfcl  16033  2ndfcl  16034  prfcl  16039  evlf2  16054  evlfcllem  16057  evlfcl  16058  curfval  16059  curf1  16061  curf12  16063  curf1cl  16064  curf2  16065  curf2val  16066  curf2cl  16067  curfcl  16068  uncfcurf  16075  hofval  16088  hof2fval  16091  hofcl  16095  yonedalem4a  16111  yonedalem3  16116  yonedainv  16117  isdlat  16390  issgrp  16479  ismndOLD  16493  ismndd  16510  grpsubfval  16659  grpsubpropd  16707  imasgrp  16753  subgsub  16780  eqgfval  16816  dpjfval  17623  issrg  17676  isring  17719  isringd  17750  dvrfval  17847  isdrngd  17935  issrngd  18024  islmodd  18032  isassa  18474  isassad  18482  asclfval  18493  ressascl  18503  psrval  18521  coe1tm  18801  evl1varpw  18884  isphld  19152  pjfval  19200  islindf  19301  scmatval  19460  mdetfval  19542  smadiadetr  19631  pmatcollpw2lem  19732  pm2mpval  19750  pm2mpghm  19771  chpmatfval  19785  cpmadugsumlemB  19829  xkohmeo  20761  xpsdsval  21327  prdsxmslem2  21475  nmfval  21534  nmpropd  21539  nmpropd2  21540  subgnm  21572  tngnm  21590  cph2di  22077  cphassr  22082  ipcau2  22101  tchcphlem2  22103  q1pval  22979  r1pval  22982  dvntaylp  23191  israg  24599  ttgval  24751  grpodivfval  25815  isrngo  25951  dipfval  26183  lnoval  26238  ressnm  28250  isslmd  28356  qqhval  28617  sitgval  28993  prdsbnd2  31831  lflset  32334  islfld  32337  ldualset  32400  cmtfvalN  32485  isoml  32513  ltrnfset  33391  trlfset  33435  docaffvalN  34398  diblss  34447  dihffval  34507  dihfval  34508  hvmapffval  35035  hvmapfval  35036  hgmapfval  35166  mendval  35748  isasslaw  38586  isrng  38634  lidlmsgrp  38684  lidlrng  38685  zlmodzxzscm  38898  lcoop  38964  lincvalsng  38969  lincvalpr  38971  lincdifsn  38977  islininds  38999
  Copyright terms: Public domain W3C validator