Metamath Proof Explorer

Theorem oveq12d

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses oveq1d.1 
|- ( ph -> A = B )
oveq12d.2 
|- ( ph -> C = D )
Assertion oveq12d 
|- ( ph -> ( A F C ) = ( B F D ) )

Proof

Step Hyp Ref Expression
1 oveq1d.1 
 |-  ( ph -> A = B )
2 oveq12d.2 
 |-  ( ph -> C = D )
3 oveq12 
 |-  ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4 1 2 3 syl2anc 
 |-  ( ph -> ( A F C ) = ( B F D ) )