Theorem oveq12i 6097

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123i  6099  1lt2nq  7773  halfnqq  7777  caucvgprprlemnbj  8060  caucvgprprlemaddq  8075  m1p1sr  8127  m1m1sr  8128  axi2m1  8242  negdii  8610  3t3e9  9462  8th4div3  9524  halfpm6th  9525  numma  9820  decmul10add  9845  4t3lem  9873  9t11e99  9906  halfthird  9919  5recm6rec  9920  fz0to3un2pr  10530  sqdivapi  11060  sq4e2t8  11074  i4  11079  binom2i  11085  facp1  11168  fac2  11169  fac3  11170  fac4  11171  4bc2eq6  11213  cji  11668  fsumadd  12173  fsumsplitf  12175  fsumsplitsnun  12186  0.999...  12288  fprodmul  12358  fprodsplitf  12399  ef01bndlem  12523  cos2bnd  12527  3dvds2dec  12633  flodddiv4  12703  nn0gcdsq  12978  pythagtriplem16  13058  4sqlem19  13188  dec5nprm  13193  dec2nprm  13194  numexp2x  13204  decsplit  13208  karatsuba  13209  2exp5  13211  2exp11  13215  2exp16  13216  ballotfilem2  13228  ballotfilemfval0  13235  ballotfilemth  13281  ecqusaddd  14041  gsummptfidmadd  14161  isrhm  14465  cnmpt2res  15398  txmetcnp  15619  dveflem  15827  efhalfpi  15900  efipi  15902  sin2pi  15904  ef2pi  15906  sincosq3sgn  15929  sincosq4sgn  15930  sinq34lt0t  15932  sincos4thpi  15941  tan4thpi  15942  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  log2tlbndlog2  16082  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  1sgm2ppw  16109  lgsdi  16156  lgsquadlem1  16196  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  ex-exp  16741  ex-fac  16742  ex-bc  16743