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 ψ φ A F C = B F D

Proof

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