Theorem oveq2i 5861

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq2i	|- ( C F A ) = ( C F B )

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq2 5858	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	ax-mp 5	1 |- ( C F A ) = ( C F B )

Syntax hints:   = wceq 1348  (class class class)co 5850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853

This theorem is referenced by:  caov32  6037  oa1suc  6443  nnm1  6500  nnm2  6501  mapsnconst  6668  mapsncnv  6669  mulidnq  7338  halfnqq  7359  addpinq1  7413  addnqpr1  7511  caucvgprlemm  7617  caucvgprprlemval  7637  caucvgprprlemnbj  7642  caucvgprprlemmu  7644  caucvgprprlemaddq  7657  caucvgprprlem1  7658  caucvgprprlem2  7659  m1p1sr  7709  m1m1sr  7710  0idsr  7716  1idsr  7717  00sr  7718  pn0sr  7720  ltm1sr  7726  caucvgsrlemoffres  7749  caucvgsr  7751  mulresr  7787  pitonnlem2  7796  axi2m1  7824  ax1rid  7826  axcnre  7830  add42i  8072  negid  8153  negsub  8154  subneg  8155  negsubdii  8191  apreap  8493  recexaplem2  8557  muleqadd  8573  crap0  8861  2p2e4  8992  3p2e5  9006  3p3e6  9007  4p2e6  9008  4p3e7  9009  4p4e8  9010  5p2e7  9011  5p3e8  9012  5p4e9  9013  6p2e8  9014  6p3e9  9015  7p2e9  9016  3t3e9  9022  8th4div3  9084  halfpm6th  9085  iap0  9088  addltmul  9101  div4p1lem1div2  9118  peano2z  9235  nn0n0n1ge2  9269  nneoor  9301  zeo  9304  numsuc  9343  numltc  9355  numsucc  9369  numma  9373  nummul1c  9378  decrmac  9387  decsubi  9392  decmul1  9393  decmul10add  9398  6p5lem  9399  5p5e10  9400  6p4e10  9401  7p3e10  9404  8p2e10  9409  4t3lem  9426  9t11e99  9459  decbin2  9470  fztp  10021  fzprval  10025  fztpval  10026  fzshftral  10051  fz0tp  10065  fz0to3un2pr  10066  fzo01  10159  fzo12sn  10160  fzo0to2pr  10161  fzo0to3tp  10162  fzo0to42pr  10163  intqfrac2  10262  intfracq  10263  sqval  10521  sq4e2t8  10560  cu2  10561  i3  10564  i4  10565  binom2i  10571  binom3  10580  3dec  10635  faclbnd  10662  faclbnd2  10663  bcn1  10679  bcn2  10685  4bc3eq4  10694  4bc2eq6  10695  reim0  10812  cji  10853  resqrexlemover  10961  resqrexlemcalc1  10965  resqrexlemcalc3  10967  absi  11010  fsump1i  11383  fsumconst  11404  modfsummodlemstep  11407  arisum2  11449  geoihalfsum  11472  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  fprodconst  11570  fprodrec  11579  ef0lem  11610  ege2le3  11621  eft0val  11643  ef4p  11644  efgt1p2  11645  efgt1p  11646  tanval2ap  11663  efival  11682  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  cos1bnd  11709  cos2bnd  11710  3dvdsdec  11811  3dvds2dec  11812  odd2np1lem  11818  odd2np1  11819  oddp1even  11822  mod2eq1n2dvds  11825  opoe  11841  6gcd4e2  11937  lcmneg  12015  3lcm2e6woprm  12027  6lcm4e12  12028  3prm  12069  3lcm2e6  12101  sqrt2irrlem  12102  pw2dvdslemn  12106  phiprm  12164  prmdiv  12176  pythagtriplem12  12216  pythagtriplem14  12218  pcfac  12289  prmpwdvds  12294  pockthi  12297  4sqlem5  12321  restin  12929  uptx  13027  cnrehmeocntop  13346  dvexp  13428  dvmptidcn  13431  dvmptccn  13432  dveflem  13440  sinhalfpilem  13465  efhalfpi  13473  cospi  13474  efipi  13475  sin2pi  13477  cos2pi  13478  ef2pi  13479  sin2pim  13487  cos2pim  13488  sinmpi  13489  cosmpi  13490  sinppi  13491  cosppi  13492  sincosq4sgn  13503  tangtx  13512  sincos4thpi  13514  sincos6thpi  13516  sincos3rdpi  13517  abssinper  13520  cosq34lt1  13524  1cxp  13574  ecxp  13575  rpcxpsqrt  13595  rpelogb  13620  2logb9irrALT  13645  binom4  13650  lgslem1  13654  lgsdir2lem1  13682  lgsdir2lem2  13683  lgsdir2lem3  13684  lgsdir2lem5  13686  lgs1  13698  2sqlem8  13712  ex-exp  13721  ex-bc  13723  ex-gcd  13725  cvgcmp2nlemabs  14024