Theorem oveq12i 6025

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 6022	. 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 1395  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq123i  6027  1lt2nq  7616  halfnqq  7620  caucvgprprlemnbj  7903  caucvgprprlemaddq  7918  m1p1sr  7970  m1m1sr  7971  axi2m1  8085  negdii  8453  3t3e9  9291  8th4div3  9353  halfpm6th  9354  numma  9644  decmul10add  9669  4t3lem  9697  9t11e99  9730  halfthird  9743  5recm6rec  9744  fz0to3un2pr  10348  sqdivapi  10875  sq4e2t8  10889  i4  10894  binom2i  10900  facp1  10982  fac2  10983  fac3  10984  fac4  10985  4bc2eq6  11026  cji  11453  fsumadd  11957  fsumsplitf  11959  fsumsplitsnun  11970  0.999...  12072  fprodmul  12142  fprodsplitf  12183  ef01bndlem  12307  cos2bnd  12311  3dvds2dec  12417  flodddiv4  12487  nn0gcdsq  12762  pythagtriplem16  12842  4sqlem19  12972  dec5nprm  12977  dec2nprm  12978  numexp2x  12988  decsplit  12992  karatsuba  12993  2exp5  12995  2exp11  12999  2exp16  13000  ecqusaddd  13815  isrhm  14162  cnmpt2res  15011  txmetcnp  15232  dveflem  15440  efhalfpi  15513  efipi  15515  sin2pi  15517  ef2pi  15519  sincosq3sgn  15542  sincosq4sgn  15543  sinq34lt0t  15545  sincos4thpi  15554  tan4thpi  15555  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  1sgm2ppw  15709  lgsdi  15756  lgsquadlem1  15796  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  ex-exp  16259  ex-fac  16260  ex-bc  16261