Theorem oveqdr

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

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

Proof

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