Theorem oveq12i 6100

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 6097	. 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 6088

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 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq123i  6102  1lt2nq  7779  halfnqq  7783  caucvgprprlemnbj  8066  caucvgprprlemaddq  8081  m1p1sr  8133  m1m1sr  8134  axi2m1  8248  negdii  8617  3t3e9  9472  8th4div3  9535  halfpm6th  9536  numma  9836  decmul10add  9861  4t3lem  9889  9t11e99  9922  halfthird  9935  5recm6rec  9936  fz0to3un2pr  10547  sqdivapi  11081  sq4e2t8  11095  i4  11100  binom2i  11106  facp1  11190  fac2  11191  fac3  11192  fac4  11193  4bc2eq6  11235  cji  11690  fsumadd  12198  fsumsplitf  12200  fsumsplitsnun  12211  0.999...  12313  fprodmul  12383  fprodsplitf  12424  ef01bndlem  12548  cos2bnd  12552  3dvds2dec  12658  flodddiv4  12728  nn0gcdsq  13005  pythagtriplem16  13087  4sqlem19  13217  dec5nprm  13222  dec2nprm  13223  mod2xnegi  13227  numexp2x  13234  decsplit  13238  karatsuba  13239  2exp5  13241  2exp11  13245  2exp16  13246  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilem2  13286  ballotfilemfval0  13293  ballotfilemth  13339  ecqusaddd  14100  gsummptfidmadd  14251  gsum2dfilem2  14272  isrhm  14574  cnmpt2res  15523  txmetcnp  15744  dveflem  15952  efhalfpi  16026  efipi  16028  sin2pi  16030  ef2pi  16032  sincosq3sgn  16055  sincosq4sgn  16056  sinq34lt0t  16058  sincos4thpi  16067  tan4thpi  16068  sincos6thpi  16069  sincos3rdpi  16070  pigt3  16071  log2tlbndlog2  16220  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  cht2  16276  cht3  16277  1sgm2ppw  16289  bclbnd  16307  bposlem8  16318  bposlem9  16319  lgsdi  16361  lgsquadlem1  16401  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  ex-exp  16946  ex-fac  16947  ex-bc  16948