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

Theorem oveq123d 6102
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 6098 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6099 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2468 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652  (class class class)co 6081
This theorem is referenced by:  csbovg  6112  prdsplusgfval  13696  prdsmulrfval  13698  prdsvscafval  13702  prdsdsval2  13706  xpsaddlem  13800  xpsvsca  13804  iscat  13897  iscatd  13898  iscatd2  13906  catcocl  13910  catass  13911  moni  13962  subccocl  14042  isfunc  14061  funcco  14068  idfucl  14078  cofuval  14079  cofuval2  14084  cofucl  14085  funcres  14093  ressffth  14135  isnat  14144  nati  14152  fuccoval  14160  coaval  14223  catcisolem  14261  xpcco  14280  xpcco2  14284  1stfcl  14294  2ndfcl  14295  prfcl  14300  evlf2  14315  evlfcllem  14318  evlfcl  14319  curfval  14320  curf1  14322  curf12  14324  curf1cl  14325  curf2  14326  curf2val  14327  curf2cl  14328  curfcl  14329  uncfcurf  14336  hofval  14349  hof2fval  14352  hofcl  14356  yonedalem4a  14372  yonedalem3  14377  yonedainv  14378  isdlat  14619  ismnd  14692  ismndd  14719  grpsubfval  14847  grpsubpropd  14889  imasgrp  14934  subgsub  14956  eqgfval  14988  dpjfval  15613  isrng  15668  isrngd  15698  dvrfval  15789  isdrngd  15860  issrngd  15949  islmodd  15956  isassa  16375  isassad  16382  asclfval  16393  ressascl  16402  psrval  16429  coe1tm  16665  isphld  16885  pjfval  16933  xkohmeo  17847  xpsdsval  18411  prdsxmslem2  18559  nmfval  18636  nmpropd  18641  nmpropd2  18642  subgnm  18674  tngnm  18692  cph2di  19169  cphassr  19174  ipcau2  19191  tchcphlem2  19193  q1pval  20076  r1pval  20079  dvntaylp  20287  grpodivfval  21830  isrngo  21966  dipfval  22198  lnoval  22253  ressnm  24184  qqhval  24358  sitgval  24647  prdsbnd2  26504  islindf  27259  mdetfval  27464  mendval  27468  lflset  29857  islfld  29860  ldualset  29923  cmtfvalN  30008  isoml  30036  ltrnfset  30914  trlfset  30957  docaffvalN  31919  diblss  31968  dihffval  32028  dihfval  32029  hvmapffval  32556  hvmapfval  32557  hgmapfval  32687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator