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	$$⊢\phi \to F=G$$
Assertion	oveqdr	$$⊢\left(\phi \wedge \psi \right)\to xFy=xGy$$

Proof

Step	Hyp	Ref	Expression
1		oveqdr.1	$$⊢\phi \to F=G$$
2	1	oveqd	$$⊢\phi \to xFy=xGy$$
3	2	adantr	$$⊢\left(\phi \wedge \psi \right)\to xFy=xGy$$