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

Theorem oveq123d 6061
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 6057 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6058 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2436 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649  (class class class)co 6040
This theorem is referenced by:  csbovg  6071  prdsplusgfval  13651  prdsmulrfval  13653  prdsvscafval  13657  prdsdsval2  13661  xpsaddlem  13755  xpsvsca  13759  iscat  13852  iscatd  13853  iscatd2  13861  catcocl  13865  catass  13866  moni  13917  subccocl  13997  isfunc  14016  funcco  14023  idfucl  14033  cofuval  14034  cofuval2  14039  cofucl  14040  funcres  14048  ressffth  14090  isnat  14099  nati  14107  fuccoval  14115  coaval  14178  catcisolem  14216  xpcco  14235  xpcco2  14239  1stfcl  14249  2ndfcl  14250  prfcl  14255  evlf2  14270  evlfcllem  14273  evlfcl  14274  curfval  14275  curf1  14277  curf12  14279  curf1cl  14280  curf2  14281  curf2val  14282  curf2cl  14283  curfcl  14284  uncfcurf  14291  hofval  14304  hof2fval  14307  hofcl  14311  yonedalem4a  14327  yonedalem3  14332  yonedainv  14333  isdlat  14574  ismnd  14647  ismndd  14674  grpsubfval  14802  grpsubpropd  14844  imasgrp  14889  subgsub  14911  eqgfval  14943  dpjfval  15568  isrng  15623  isrngd  15653  dvrfval  15744  isdrngd  15815  issrngd  15904  islmodd  15911  isassa  16330  isassad  16337  asclfval  16348  ressascl  16357  psrval  16384  coe1tm  16620  isphld  16840  pjfval  16888  xkohmeo  17800  xpsdsval  18364  prdsxmslem2  18512  nmfval  18589  nmpropd  18594  nmpropd2  18595  subgnm  18627  tngnm  18645  cph2di  19122  cphassr  19127  ipcau2  19144  tchcphlem2  19146  q1pval  20029  r1pval  20032  dvntaylp  20240  grpodivfval  21783  isrngo  21919  dipfval  22151  lnoval  22206  ressnm  24137  qqhval  24311  sitgval  24600  prdsbnd2  26394  islindf  27150  mdetfval  27355  mendval  27359  lflset  29542  islfld  29545  ldualset  29608  cmtfvalN  29693  isoml  29721  ltrnfset  30599  trlfset  30642  docaffvalN  31604  diblss  31653  dihffval  31713  dihfval  31714  hvmapffval  32241  hvmapfval  32242  hgmapfval  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator