Theorem oveq12i 6071

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 6068	. 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 1398  (class class class)co 6059

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-br 4116  df-iota 5318  df-fv 5366  df-ov 6062

This theorem is referenced by:  oveq123i  6073  1lt2nq  7738  halfnqq  7742  caucvgprprlemnbj  8025  caucvgprprlemaddq  8040  m1p1sr  8092  m1m1sr  8093  axi2m1  8207  negdii  8575  3t3e9  9416  8th4div3  9478  halfpm6th  9479  numma  9774  decmul10add  9799  4t3lem  9827  9t11e99  9860  halfthird  9873  5recm6rec  9874  fz0to3un2pr  10483  sqdivapi  11013  sq4e2t8  11027  i4  11032  binom2i  11038  facp1  11121  fac2  11122  fac3  11123  fac4  11124  4bc2eq6  11166  cji  11617  fsumadd  12122  fsumsplitf  12124  fsumsplitsnun  12135  0.999...  12237  fprodmul  12307  fprodsplitf  12348  ef01bndlem  12472  cos2bnd  12476  3dvds2dec  12582  flodddiv4  12652  nn0gcdsq  12927  pythagtriplem16  13007  4sqlem19  13137  dec5nprm  13142  dec2nprm  13143  numexp2x  13153  decsplit  13157  karatsuba  13158  2exp5  13160  2exp11  13164  2exp16  13165  ballotfilem2  13177  ballotfilemfval0  13184  ballotfilemth  13230  ecqusaddd  13996  isrhm  14408  cnmpt2res  15293  txmetcnp  15514  dveflem  15722  efhalfpi  15795  efipi  15797  sin2pi  15799  ef2pi  15801  sincosq3sgn  15824  sincosq4sgn  15825  sinq34lt0t  15827  sincos4thpi  15836  tan4thpi  15837  sincos6thpi  15838  sincos3rdpi  15839  pigt3  15840  1sgm2ppw  15994  lgsdi  16041  lgsquadlem1  16081  2lgsoddprmlem3c  16113  2lgsoddprmlem3d  16114  ex-exp  16626  ex-fac  16627  ex-bc  16628