Theorem oveq12i 6013

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 6010	. 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 6001

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  oveq123i  6015  1lt2nq  7593  halfnqq  7597  caucvgprprlemnbj  7880  caucvgprprlemaddq  7895  m1p1sr  7947  m1m1sr  7948  axi2m1  8062  negdii  8430  3t3e9  9268  8th4div3  9330  halfpm6th  9331  numma  9621  decmul10add  9646  4t3lem  9674  9t11e99  9707  halfthird  9720  5recm6rec  9721  fz0to3un2pr  10319  sqdivapi  10845  sq4e2t8  10859  i4  10864  binom2i  10870  facp1  10952  fac2  10953  fac3  10954  fac4  10955  4bc2eq6  10996  cji  11413  fsumadd  11917  fsumsplitf  11919  fsumsplitsnun  11930  0.999...  12032  fprodmul  12102  fprodsplitf  12143  ef01bndlem  12267  cos2bnd  12271  3dvds2dec  12377  flodddiv4  12447  nn0gcdsq  12722  pythagtriplem16  12802  4sqlem19  12932  dec5nprm  12937  dec2nprm  12938  numexp2x  12948  decsplit  12952  karatsuba  12953  2exp5  12955  2exp11  12959  2exp16  12960  ecqusaddd  13775  isrhm  14122  cnmpt2res  14971  txmetcnp  15192  dveflem  15400  efhalfpi  15473  efipi  15475  sin2pi  15477  ef2pi  15479  sincosq3sgn  15502  sincosq4sgn  15503  sinq34lt0t  15505  sincos4thpi  15514  tan4thpi  15515  sincos6thpi  15516  sincos3rdpi  15517  pigt3  15518  1sgm2ppw  15669  lgsdi  15716  lgsquadlem1  15756  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  ex-exp  16091  ex-fac  16092  ex-bc  16093