Theorem oveq12i 5794

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 5791	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	mp2an 423	1 |- ( A F C ) = ( B F D )

Syntax hints:   = wceq 1332  (class class class)co 5782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  oveq123i  5796  1lt2nq  7238  halfnqq  7242  caucvgprprlemnbj  7525  caucvgprprlemaddq  7540  m1p1sr  7592  m1m1sr  7593  axi2m1  7707  negdii  8070  3t3e9  8901  8th4div3  8963  halfpm6th  8964  numma  9249  decmul10add  9274  4t3lem  9302  9t11e99  9335  halfthird  9348  5recm6rec  9349  sqdivapi  10407  sq4e2t8  10421  i4  10426  binom2i  10432  facp1  10508  fac2  10509  fac3  10510  fac4  10511  4bc2eq6  10552  cji  10706  fsumadd  11207  fsumsplitf  11209  fsumsplitsnun  11220  0.999...  11322  ef01bndlem  11499  cos2bnd  11503  3dvds2dec  11599  flodddiv4  11667  nn0gcdsq  11914  cnmpt2res  12505  txmetcnp  12726  dveflem  12895  efhalfpi  12928  efipi  12930  sin2pi  12932  ef2pi  12934  sincosq3sgn  12957  sincosq4sgn  12958  sinq34lt0t  12960  sincos4thpi  12969  tan4thpi  12970  sincos6thpi  12971  sincos3rdpi  12972  pigt3  12973  ex-exp  13110  ex-fac  13111  ex-bc  13112