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 φF=G
Assertion oveqdr φψxFy=xGy

Proof

Step Hyp Ref Expression
1 oveqdr.1 φF=G
2 1 oveqd φxFy=xGy
3 2 adantr φψxFy=xGy