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

Theorem oveq123d 5879
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 5875 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 5876 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2315 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  csbovg  5889  prdsplusgfval  13373  prdsmulrfval  13375  prdsvscafval  13379  prdsdsval2  13383  xpsaddlem  13477  xpsvsca  13481  iscat  13574  iscatd  13575  iscatd2  13583  catcocl  13587  catass  13588  moni  13639  subccocl  13719  isfunc  13738  funcco  13745  idfucl  13755  cofuval  13756  cofuval2  13761  cofucl  13762  funcres  13770  ressffth  13812  isnat  13821  nati  13829  fuccoval  13837  coaval  13900  catcisolem  13938  xpcco  13957  xpcco2  13961  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlf2  13992  evlfcllem  13995  evlfcl  13996  curfval  13997  curf1  13999  curf12  14001  curf1cl  14002  curf2  14003  curf2val  14004  curf2cl  14005  curfcl  14006  uncfcurf  14013  hofval  14026  hof2fval  14029  hofcl  14033  yonedalem4a  14049  yonedalem3  14054  yonedainv  14055  isdlat  14296  ismnd  14369  ismndd  14396  grpsubfval  14524  grpsubpropd  14566  imasgrp  14611  subgsub  14633  eqgfval  14665  dpjfval  15290  isrng  15345  isrngd  15375  dvrfval  15466  isdrngd  15537  issrngd  15626  islmodd  15633  isassa  16056  isassad  16063  asclfval  16074  ressascl  16083  psrval  16110  coe1tm  16349  isphld  16558  pjfval  16606  xkohmeo  17506  xpsdsval  17945  prdsxmslem2  18075  nmfval  18111  nmpropd  18116  nmpropd2  18117  subgnm  18149  tngnm  18167  cph2di  18642  cphassr  18647  ipcau2  18664  tchcphlem2  18666  q1pval  19539  r1pval  19542  dvntaylp  19750  grpodivfval  20909  isrngo  21045  dipfval  21275  lnoval  21330  islatalg  25183  vecval1b  25451  vecval3b  25452  isucv  25677  isdivcv2  25693  isder  25707  isntr  25873  islimcat  25876  isray  26154  prdsbnd2  26519  islindf  27282  mdetfval  27487  mendval  27491  lflset  29249  islfld  29252  ldualset  29315  cmtfvalN  29400  isoml  29428  ltrnfset  30306  trlfset  30349  docaffvalN  31311  diblss  31360  dihffval  31420  dihfval  31421  hvmapffval  31948  hvmapfval  31949  hgmapfval  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator