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 454 1  |-  ( ( ps  /\  ph )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437  (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 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299
This theorem is referenced by:  addpipq  9351  mulgt0sr  9518  mulcnsr  9549  mulresr  9552  recdiv  10302  revccat  12845  rlimdiv  13676  caucvg  13712  estrchom  15956  funcestrcsetclem5  15973  ismhm  16528  mpfrcl  18669  xrsdsval  18940  matval  19360  ucnval  21216  volcn  22438  dvres2lem  22739  dvid  22746  c1lip3  22825  taylthlem1  23190  abelthlem9  23257  brbtwn2  24778  nonbooli  27136  0cnop  27464  0cnfn  27465  idcnop  27466  bccolsum  30159  ftc1anc  31729  rmydioph  35579  expdiophlem2  35587  dvcosax  37374  ismgmhm  38554  2zrngamgm  38710  rnghmsscmap2  38746  rnghmsscmap  38747  funcrngcsetc  38771  rhmsscmap2  38792  rhmsscmap  38793  funcringcsetc  38808
  Copyright terms: Public domain W3C validator