This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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