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

Theorem oveq123d 6117
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 6113 . 2  |-  ( ph  ->  ( A F C )  =  ( A G C ) )
3 oveq123d.2 . . 3  |-  ( ph  ->  A  =  B )
4 oveq123d.3 . . 3  |-  ( ph  ->  C  =  D )
53, 4oveq12d 6114 . 2  |-  ( ph  ->  ( A G C )  =  ( B G D ) )
62, 5eqtrd 2475 1  |-  ( ph  ->  ( A F C )  =  ( B G D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369  (class class class)co 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-iota 5386  df-fv 5431  df-ov 6099
This theorem is referenced by:  csbov123  6127  csbovgOLD  6129  prdsplusgfval  14417  prdsmulrfval  14419  prdsvscafval  14423  prdsdsval2  14427  xpsaddlem  14518  xpsvsca  14522  iscat  14615  iscatd  14616  iscatd2  14624  catcocl  14628  catass  14629  moni  14680  subccocl  14760  isfunc  14779  funcco  14786  idfucl  14796  cofuval  14797  cofuval2  14802  cofucl  14803  funcres  14811  ressffth  14853  isnat  14862  nati  14870  fuccoval  14878  coaval  14941  catcisolem  14979  xpcco  14998  xpcco2  15002  1stfcl  15012  2ndfcl  15013  prfcl  15018  evlf2  15033  evlfcllem  15036  evlfcl  15037  curfval  15038  curf1  15040  curf12  15042  curf1cl  15043  curf2  15044  curf2val  15045  curf2cl  15046  curfcl  15047  uncfcurf  15054  hofval  15067  hof2fval  15070  hofcl  15074  yonedalem4a  15090  yonedalem3  15095  yonedainv  15096  isdlat  15368  ismnd  15422  ismndd  15449  grpsubfval  15585  grpsubpropd  15631  imasgrp  15676  subgsub  15698  eqgfval  15734  dpjfval  16559  issrg  16614  isrng  16654  isrngd  16684  dvrfval  16781  isdrngd  16862  issrngd  16951  islmodd  16959  isassa  17392  isassad  17399  asclfval  17410  ressascl  17419  psrval  17434  coe1tm  17731  evl1varpw  17800  isphld  18088  pjfval  18136  islindf  18246  mdetfval  18402  smadiadetr  18486  xkohmeo  19393  xpsdsval  19961  prdsxmslem2  20109  nmfval  20186  nmpropd  20191  nmpropd2  20192  subgnm  20224  tngnm  20242  cph2di  20730  cphassr  20735  ipcau2  20754  tchcphlem2  20756  q1pval  21630  r1pval  21633  dvntaylp  21841  israg  23096  ttgval  23126  grpodivfval  23734  isrngo  23870  dipfval  24102  lnoval  24157  ressnm  26117  isslmd  26223  qqhval  26408  sitgval  26723  prdsbnd2  28699  mendval  29545  zlmodzxzscm  30759  pmatcollpw2lem  30910  pmattomply1ghm  30930  pmattomply1mhmlem2  30934  lcoop  30950  lincvalsng  30955  lincvalpr  30957  lincdifsn  30963  islininds  30985  lflset  32709  islfld  32712  ldualset  32775  cmtfvalN  32860  isoml  32888  ltrnfset  33766  trlfset  33809  docaffvalN  34771  diblss  34820  dihffval  34880  dihfval  34881  hvmapffval  35408  hvmapfval  35409  hgmapfval  35539
  Copyright terms: Public domain W3C validator