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

Step	Hyp	Ref	Expression
1		oveq1d.1	. . 3
2		opreqan12i.2	. . 3
3	1, 2	oveqan12d 6315	. 2
4	3	ancoms 453	1

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