Theorem oveqdr 6107

Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)

Hypothesis

Ref	Expression
oveqdr.1	|- ( ph -> F = G )

Assertion

Ref	Expression
oveqdr	|- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )

Proof of Theorem oveqdr

Step	Hyp	Ref	Expression
1		oveqdr.1	. . 3 |- ( ph -> F = G )
2	1	oveqd 6096	. 2 |- ( ph -> ( x F y ) = ( x G y ) )
3	2	adantr 276	1 |- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402  (class class class)co 6079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082

This theorem is referenced by:  grppropstrg  13807  grpsubpropdg  13892  isrngd  14235  crngpropd  14327  isringd  14329  ring1  14347  opprrng  14365  opprrngbg  14366  opprring  14367  opprringbg  14368  opprsubgg  14373  mulgass3  14374  rngidpropdg  14436  invrpropdg  14439  subrngpropd  14507  subrgpropd  14544  isdomn  14561  aprprop  14584  sraring  14769  sralmod  14770  sralmod0g  14771  issubrgd  14772  rlmvnegg  14785  lidlrsppropdg  14815  crngridl  14850  znzrh  14961  zncrng  14963