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	$⊢ φ \to F = G$
	Assertion	oveqdr	$⊢ (φ \land ψ) \to x F y = x G y$

Proof

Step	Hyp	Ref	Expression
1		oveqdr.1	$⊢ φ \to F = G$
2	1	oveqd	$⊢ φ \to x F y = x G y$
3	2	adantr	$⊢ (φ \land ψ) \to x F y = x G y$