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

Theorem oveqan12rd 6316
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1  |-  ( ph  ->  A  =  B )
opreqan12i.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
oveqan12rd  |-  ( ( ps  /\  ph )  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveqan12rd
StepHypRef Expression
1 oveq1d.1 . . 3  |-  ( ph  ->  A  =  B )
2 opreqan12i.2 . . 3  |-  ( ps 
->  C  =  D
)
31, 2oveqan12d 6315 . 2  |-  ( (
ph  /\  ps )  ->  ( A F C )  =  ( B F D ) )
43ancoms 453 1  |-  ( ( ps  /\  ph )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395  (class class class)co 6296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299
This theorem is referenced by:  addpipq  9332  mulgt0sr  9499  mulcnsr  9530  mulresr  9533  recdiv  10271  revccat  12751  rlimdiv  13479  caucvg  13512  estrchom  15522  funcestrcsetclem5  15539  ismhm  16094  mpfrcl  18313  xrsdsval  18588  matval  19039  ucnval  20905  volcn  22140  dvres2lem  22439  dvid  22446  c1lip3  22525  taylthlem1  22893  abelthlem9  22960  brbtwn2  24334  nonbooli  26695  0cnop  27024  0cnfn  27025  idcnop  27026  ftc1anc  30260  rmydioph  31118  expdiophlem2  31126  dvcosax  31884  ismgmhm  32691  2zrngamgm  32847  rnghmsscmap2  32883  rnghmsscmap  32884  funcrngcsetc  32908  rhmsscmap2  32929  rhmsscmap  32930  funcringcsetc  32945
  Copyright terms: Public domain W3C validator