This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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