Theorem oveqdr 6116

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 6105	. 2 |- ( ph -> ( x F y ) = ( x G y ) )
3	2	adantr 276	1 |- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402  (class class class)co 6088

This proof depends on 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 proof 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 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  grppropstrg  13884  grpsubpropdg  13969  isrngd  14360  crngpropd  14452  isringd  14454  ring1  14472  opprrng  14492  opprrngbg  14493  opprring  14494  opprringbg  14495  opprsubgg  14500  mulgass3  14501  rngidpropdg  14563  invrpropdg  14566  subrngpropd  14634  subrgpropd  14671  isdomn  14688  aprprop  14711  sraring  14896  sralmod  14897  sralmod0g  14898  issubrgd  14899  rlmvnegg  14912  lidlrsppropdg  14942  crngridl  14977  znzrh  15088  zncrng  15090