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

Theorem oveqan12rd 6111
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 6110 . 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 1369  (class class class)co 6091
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 2568  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  addpipq  9106  mulgt0sr  9272  mulcnsr  9303  mulresr  9306  recdiv  10037  revccat  12406  rlimdiv  13123  caucvg  13156  ismhm  15466  mpfrcl  17604  xrsdsval  17857  matval  18311  ucnval  19852  volcn  21086  dvres2lem  21385  dvid  21392  c1lip3  21471  taylthlem1  21838  abelthlem9  21905  brbtwn2  23151  nonbooli  25054  0cnop  25383  0cnfn  25384  idcnop  25385  ftc1anc  28475  rmydioph  29363  expdiophlem2  29371
  Copyright terms: Public domain W3C validator