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	⊢ ( 𝜑 → 𝐹 = 𝐺 )
Assertion	oveqdr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		oveqdr.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2	1	oveqd	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )