Theorem oveq2i 5852

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 5849	. 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 1343  (class class class)co 5841

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  caov32  6025  oa1suc  6431  nnm1  6488  nnm2  6489  mapsnconst  6656  mapsncnv  6657  mulidnq  7326  halfnqq  7347  addpinq1  7401  addnqpr1  7499  caucvgprlemm  7605  caucvgprprlemval  7625  caucvgprprlemnbj  7630  caucvgprprlemmu  7632  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  m1p1sr  7697  m1m1sr  7698  0idsr  7704  1idsr  7705  00sr  7706  pn0sr  7708  ltm1sr  7714  caucvgsrlemoffres  7737  caucvgsr  7739  mulresr  7775  pitonnlem2  7784  axi2m1  7812  ax1rid  7814  axcnre  7818  add42i  8060  negid  8141  negsub  8142  subneg  8143  negsubdii  8179  apreap  8481  recexaplem2  8545  muleqadd  8561  crap0  8849  2p2e4  8980  3p2e5  8994  3p3e6  8995  4p2e6  8996  4p3e7  8997  4p4e8  8998  5p2e7  8999  5p3e8  9000  5p4e9  9001  6p2e8  9002  6p3e9  9003  7p2e9  9004  3t3e9  9010  8th4div3  9072  halfpm6th  9073  iap0  9076  addltmul  9089  div4p1lem1div2  9106  peano2z  9223  nn0n0n1ge2  9257  nneoor  9289  zeo  9292  numsuc  9331  numltc  9343  numsucc  9357  numma  9361  nummul1c  9366  decrmac  9375  decsubi  9380  decmul1  9381  decmul10add  9386  6p5lem  9387  5p5e10  9388  6p4e10  9389  7p3e10  9392  8p2e10  9397  4t3lem  9414  9t11e99  9447  decbin2  9458  fztp  10009  fzprval  10013  fztpval  10014  fzshftral  10039  fz0tp  10053  fz0to3un2pr  10054  fzo01  10147  fzo12sn  10148  fzo0to2pr  10149  fzo0to3tp  10150  fzo0to42pr  10151  intqfrac2  10250  intfracq  10251  sqval  10509  sq4e2t8  10548  cu2  10549  i3  10552  i4  10553  binom2i  10559  binom3  10568  3dec  10623  faclbnd  10650  faclbnd2  10651  bcn1  10667  bcn2  10673  4bc3eq4  10682  4bc2eq6  10683  reim0  10799  cji  10840  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemcalc3  10954  absi  10997  fsump1i  11370  fsumconst  11391  modfsummodlemstep  11394  arisum2  11436  geoihalfsum  11459  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  fprodconst  11557  fprodrec  11566  ef0lem  11597  ege2le3  11608  eft0val  11630  ef4p  11631  efgt1p2  11632  efgt1p  11633  tanval2ap  11650  efival  11669  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  cos1bnd  11696  cos2bnd  11697  3dvdsdec  11798  3dvds2dec  11799  odd2np1lem  11805  odd2np1  11806  oddp1even  11809  mod2eq1n2dvds  11812  opoe  11828  6gcd4e2  11924  lcmneg  12002  3lcm2e6woprm  12014  6lcm4e12  12015  3prm  12056  3lcm2e6  12088  sqrt2irrlem  12089  pw2dvdslemn  12093  phiprm  12151  prmdiv  12163  pythagtriplem12  12203  pythagtriplem14  12205  pcfac  12276  prmpwdvds  12281  pockthi  12284  4sqlem5  12308  restin  12776  uptx  12874  cnrehmeocntop  13193  dvexp  13275  dvmptidcn  13278  dvmptccn  13279  dveflem  13287  sinhalfpilem  13312  efhalfpi  13320  cospi  13321  efipi  13322  sin2pi  13324  cos2pi  13325  ef2pi  13326  sin2pim  13334  cos2pim  13335  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  sincosq4sgn  13350  tangtx  13359  sincos4thpi  13361  sincos6thpi  13363  sincos3rdpi  13364  abssinper  13367  cosq34lt1  13371  1cxp  13421  ecxp  13422  rpcxpsqrt  13442  rpelogb  13467  2logb9irrALT  13492  binom4  13497  lgslem1  13501  lgsdir2lem1  13529  lgsdir2lem2  13530  lgsdir2lem3  13531  lgsdir2lem5  13533  lgs1  13545  2sqlem8  13559  ex-exp  13568  ex-bc  13570  ex-gcd  13572  cvgcmp2nlemabs  13871