Theorem oveq12i 5884

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

Hypotheses

Ref	Expression
oveq1i.1	|- A = B
oveq12i.2	|- C = D

Assertion

Ref	Expression
oveq12i	|- ( A F C ) = ( B F D )

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq12i.2	. 2 |- C = D
3		oveq12 5881	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	mp2an 426	1 |- ( A F C ) = ( B F D )

Syntax hints:   = wceq 1353  (class class class)co 5872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-iota 5177  df-fv 5223  df-ov 5875

This theorem is referenced by:  oveq123i  5886  1lt2nq  7402  halfnqq  7406  caucvgprprlemnbj  7689  caucvgprprlemaddq  7704  m1p1sr  7756  m1m1sr  7757  axi2m1  7871  negdii  8237  3t3e9  9072  8th4div3  9134  halfpm6th  9135  numma  9423  decmul10add  9448  4t3lem  9476  9t11e99  9509  halfthird  9522  5recm6rec  9523  fz0to3un2pr  10118  sqdivapi  10598  sq4e2t8  10612  i4  10617  binom2i  10623  facp1  10703  fac2  10704  fac3  10705  fac4  10706  4bc2eq6  10747  cji  10904  fsumadd  11407  fsumsplitf  11409  fsumsplitsnun  11420  0.999...  11522  fprodmul  11592  fprodsplitf  11633  ef01bndlem  11757  cos2bnd  11761  3dvds2dec  11863  flodddiv4  11931  nn0gcdsq  12192  pythagtriplem16  12271  cnmpt2res  13668  txmetcnp  13889  dveflem  14058  efhalfpi  14091  efipi  14093  sin2pi  14095  ef2pi  14097  sincosq3sgn  14120  sincosq4sgn  14121  sinq34lt0t  14123  sincos4thpi  14132  tan4thpi  14133  sincos6thpi  14134  sincos3rdpi  14135  pigt3  14136  lgsdi  14309  ex-exp  14339  ex-fac  14340  ex-bc  14341