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

Theorem oveq123d 6101
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 6097 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6098 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2465 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362  (class class class)co 6080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  csbov123  6111  csbovgOLD  6113  prdsplusgfval  14394  prdsmulrfval  14396  prdsvscafval  14400  prdsdsval2  14404  xpsaddlem  14495  xpsvsca  14499  iscat  14592  iscatd  14593  iscatd2  14601  catcocl  14605  catass  14606  moni  14657  subccocl  14737  isfunc  14756  funcco  14763  idfucl  14773  cofuval  14774  cofuval2  14779  cofucl  14780  funcres  14788  ressffth  14830  isnat  14839  nati  14847  fuccoval  14855  coaval  14918  catcisolem  14956  xpcco  14975  xpcco2  14979  1stfcl  14989  2ndfcl  14990  prfcl  14995  evlf2  15010  evlfcllem  15013  evlfcl  15014  curfval  15015  curf1  15017  curf12  15019  curf1cl  15020  curf2  15021  curf2val  15022  curf2cl  15023  curfcl  15024  uncfcurf  15031  hofval  15044  hof2fval  15047  hofcl  15051  yonedalem4a  15067  yonedalem3  15072  yonedainv  15073  isdlat  15345  ismnd  15399  ismndd  15426  grpsubfval  15559  grpsubpropd  15605  imasgrp  15650  subgsub  15672  eqgfval  15708  dpjfval  16527  isrng  16584  isrngd  16614  dvrfval  16709  isdrngd  16780  issrngd  16869  islmodd  16877  isassa  17308  isassad  17315  asclfval  17326  ressascl  17335  psrval  17362  coe1tm  17623  isphld  17924  pjfval  17972  islindf  18082  mdetfval  18238  smadiadetr  18322  xkohmeo  19229  xpsdsval  19797  prdsxmslem2  19945  nmfval  20022  nmpropd  20027  nmpropd2  20028  subgnm  20060  tngnm  20078  cph2di  20566  cphassr  20571  ipcau2  20590  tchcphlem2  20592  q1pval  21509  r1pval  21512  dvntaylp  21720  ttgval  22943  grpodivfval  23551  isrngo  23687  dipfval  23919  lnoval  23974  ressnm  25934  issrg  26041  isslmd  26066  qqhval  26256  sitgval  26565  prdsbnd2  28535  mendval  29382  zlmodzxzscm  30585  lcoop  30651  lincvalsng  30656  lincvalpr  30658  lincdifsn  30664  islininds  30686  lflset  32274  islfld  32277  ldualset  32340  cmtfvalN  32425  isoml  32453  ltrnfset  33331  trlfset  33374  docaffvalN  34336  diblss  34385  dihffval  34445  dihfval  34446  hvmapffval  34973  hvmapfval  34974  hgmapfval  35104
  Copyright terms: Public domain W3C validator