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

Theorem oveqan12rd 6316
 Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1
opreqan12i.2
Assertion
Ref Expression
oveqan12rd

Proof of Theorem oveqan12rd
StepHypRef Expression
1 oveq1d.1 . . 3
2 opreqan12i.2 . . 3
31, 2oveqan12d 6315 . 2
43ancoms 453 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  (class class class)co 6296 This theorem is referenced by:  addpipq  9336  mulgt0sr  9503  mulcnsr  9534  mulresr  9537  recdiv  10275  revccat  12740  rlimdiv  13468  caucvg  13501  ismhm  15968  mpfrcl  18187  xrsdsval  18462  matval  18913  ucnval  20780  volcn  22015  dvres2lem  22314  dvid  22321  c1lip3  22400  taylthlem1  22768  abelthlem9  22835  brbtwn2  24208  nonbooli  26569  0cnop  26898  0cnfn  26899  idcnop  26900  ftc1anc  30098  rmydioph  30956  expdiophlem2  30964  dvcosax  31723  ismgmhm  32471  estrchom  32633  funcestrcsetclem5  32650  2zrngamgm  32745  rnghmsscmap2  32781  rnghmsscmap  32782  funcrngcsetc  32806  rhmsscmap2  32827  rhmsscmap  32828  funcringcsetc  32843 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  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 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
 Copyright terms: Public domain W3C validator