Theorem oveq12i 5837

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 5834	. 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 1335  (class class class)co 5825

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-br 3967  df-iota 5136  df-fv 5179  df-ov 5828

This theorem is referenced by:  oveq123i  5839  1lt2nq  7327  halfnqq  7331  caucvgprprlemnbj  7614  caucvgprprlemaddq  7629  m1p1sr  7681  m1m1sr  7682  axi2m1  7796  negdii  8160  3t3e9  8991  8th4div3  9053  halfpm6th  9054  numma  9339  decmul10add  9364  4t3lem  9392  9t11e99  9425  halfthird  9438  5recm6rec  9439  fz0to3un2pr  10026  sqdivapi  10506  sq4e2t8  10520  i4  10525  binom2i  10531  facp1  10608  fac2  10609  fac3  10610  fac4  10611  4bc2eq6  10652  cji  10806  fsumadd  11307  fsumsplitf  11309  fsumsplitsnun  11320  0.999...  11422  fprodmul  11492  fprodsplitf  11533  ef01bndlem  11657  cos2bnd  11661  3dvds2dec  11761  flodddiv4  11829  nn0gcdsq  12079  pythagtriplem16  12158  cnmpt2res  12739  txmetcnp  12960  dveflem  13129  efhalfpi  13162  efipi  13164  sin2pi  13166  ef2pi  13168  sincosq3sgn  13191  sincosq4sgn  13192  sinq34lt0t  13194  sincos4thpi  13203  tan4thpi  13204  sincos6thpi  13205  sincos3rdpi  13206  pigt3  13207  ex-exp  13345  ex-fac  13346  ex-bc  13347