Theorem oveq12i 5979

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 5976	. 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 1373  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  oveq123i  5981  1lt2nq  7554  halfnqq  7558  caucvgprprlemnbj  7841  caucvgprprlemaddq  7856  m1p1sr  7908  m1m1sr  7909  axi2m1  8023  negdii  8391  3t3e9  9229  8th4div3  9291  halfpm6th  9292  numma  9582  decmul10add  9607  4t3lem  9635  9t11e99  9668  halfthird  9681  5recm6rec  9682  fz0to3un2pr  10280  sqdivapi  10805  sq4e2t8  10819  i4  10824  binom2i  10830  facp1  10912  fac2  10913  fac3  10914  fac4  10915  4bc2eq6  10956  cji  11328  fsumadd  11832  fsumsplitf  11834  fsumsplitsnun  11845  0.999...  11947  fprodmul  12017  fprodsplitf  12058  ef01bndlem  12182  cos2bnd  12186  3dvds2dec  12292  flodddiv4  12362  nn0gcdsq  12637  pythagtriplem16  12717  4sqlem19  12847  dec5nprm  12852  dec2nprm  12853  numexp2x  12863  decsplit  12867  karatsuba  12868  2exp5  12870  2exp11  12874  2exp16  12875  ecqusaddd  13689  isrhm  14035  cnmpt2res  14884  txmetcnp  15105  dveflem  15313  efhalfpi  15386  efipi  15388  sin2pi  15390  ef2pi  15392  sincosq3sgn  15415  sincosq4sgn  15416  sinq34lt0t  15418  sincos4thpi  15427  tan4thpi  15428  sincos6thpi  15429  sincos3rdpi  15430  pigt3  15431  1sgm2ppw  15582  lgsdi  15629  lgsquadlem1  15669  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  ex-exp  15863  ex-fac  15864  ex-bc  15865