**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 | $${\u22a2}{\phi}\to {F}={G}$$ | |

Assertion | oveqdr | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {x}{F}{y}={x}{G}{y}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | oveqdr.1 | $${\u22a2}{\phi}\to {F}={G}$$ | |

2 | 1 | oveqd | $${\u22a2}{\phi}\to {x}{F}{y}={x}{G}{y}$$ |

3 | 2 | adantr | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {x}{F}{y}={x}{G}{y}$$ |