Metamath Proof Explorer


Theorem oveqan12rd

Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995)

Ref Expression
Hypotheses oveq1d.1 φA=B
opreqan12i.2 ψC=D
Assertion oveqan12rd ψφAFC=BFD

Proof

Step Hyp Ref Expression
1 oveq1d.1 φA=B
2 opreqan12i.2 ψC=D
3 1 2 oveqan12d φψAFC=BFD
4 3 ancoms ψφAFC=BFD