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

Metamath Proof Explorer

Theorem oveq12i

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses oveq1i.1 ⊢ A = B
oveq12i.2 ⊢ C = D
Assertion oveq12i ⊢ A F C = B F D

Proof

Step Hyp Ref Expression
1 oveq1i.1 ⊢ A = B
2 oveq12i.2 ⊢ C = D
3 oveq12 ⊢ A = B ∧ C = D → A F C = B F D
4 1 2 3 mp2an ⊢ A F C = B F D