Theorem oveq2i 5880

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 5877	. 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 1353  (class class class)co 5869

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872

This theorem is referenced by:  caov32  6056  oa1suc  6462  nnm1  6520  nnm2  6521  mapsnconst  6688  mapsncnv  6689  mulidnq  7379  halfnqq  7400  addpinq1  7454  addnqpr1  7552  caucvgprlemm  7658  caucvgprprlemval  7678  caucvgprprlemnbj  7683  caucvgprprlemmu  7685  caucvgprprlemaddq  7698  caucvgprprlem1  7699  caucvgprprlem2  7700  m1p1sr  7750  m1m1sr  7751  0idsr  7757  1idsr  7758  00sr  7759  pn0sr  7761  ltm1sr  7767  caucvgsrlemoffres  7790  caucvgsr  7792  mulresr  7828  pitonnlem2  7837  axi2m1  7865  ax1rid  7867  axcnre  7871  add42i  8113  negid  8194  negsub  8195  subneg  8196  negsubdii  8232  apreap  8534  recexaplem2  8598  muleqadd  8614  crap0  8904  2p2e4  9035  3p2e5  9049  3p3e6  9050  4p2e6  9051  4p3e7  9052  4p4e8  9053  5p2e7  9054  5p3e8  9055  5p4e9  9056  6p2e8  9057  6p3e9  9058  7p2e9  9059  3t3e9  9065  8th4div3  9127  halfpm6th  9128  iap0  9131  addltmul  9144  div4p1lem1div2  9161  peano2z  9278  nn0n0n1ge2  9312  nneoor  9344  zeo  9347  numsuc  9386  numltc  9398  numsucc  9412  numma  9416  nummul1c  9421  decrmac  9430  decsubi  9435  decmul1  9436  decmul10add  9441  6p5lem  9442  5p5e10  9443  6p4e10  9444  7p3e10  9447  8p2e10  9452  4t3lem  9469  9t11e99  9502  decbin2  9513  fztp  10064  fzprval  10068  fztpval  10069  fzshftral  10094  fz0tp  10108  fz0to3un2pr  10109  fzo01  10202  fzo12sn  10203  fzo0to2pr  10204  fzo0to3tp  10205  fzo0to42pr  10206  intqfrac2  10305  intfracq  10306  sqval  10564  sq4e2t8  10603  cu2  10604  i3  10607  i4  10608  binom2i  10614  binom3  10623  3dec  10678  faclbnd  10705  faclbnd2  10706  bcn1  10722  bcn2  10728  4bc3eq4  10737  4bc2eq6  10738  reim0  10854  cji  10895  resqrexlemover  11003  resqrexlemcalc1  11007  resqrexlemcalc3  11009  absi  11052  fsump1i  11425  fsumconst  11446  modfsummodlemstep  11449  arisum2  11491  geoihalfsum  11514  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  fprodconst  11612  fprodrec  11621  ef0lem  11652  ege2le3  11663  eft0val  11685  ef4p  11686  efgt1p2  11687  efgt1p  11688  tanval2ap  11705  efival  11724  ef01bndlem  11748  sin01bnd  11749  cos01bnd  11750  cos1bnd  11751  cos2bnd  11752  3dvdsdec  11853  3dvds2dec  11854  odd2np1lem  11860  odd2np1  11861  oddp1even  11864  mod2eq1n2dvds  11867  opoe  11883  6gcd4e2  11979  lcmneg  12057  3lcm2e6woprm  12069  6lcm4e12  12070  3prm  12111  3lcm2e6  12143  sqrt2irrlem  12144  pw2dvdslemn  12148  phiprm  12206  prmdiv  12218  pythagtriplem12  12258  pythagtriplem14  12260  pcfac  12331  prmpwdvds  12336  pockthi  12339  4sqlem5  12363  ressval2  12508  restin  13343  uptx  13441  cnrehmeocntop  13760  dvexp  13842  dvmptidcn  13845  dvmptccn  13846  dveflem  13854  sinhalfpilem  13879  efhalfpi  13887  cospi  13888  efipi  13889  sin2pi  13891  cos2pi  13892  ef2pi  13893  sin2pim  13901  cos2pim  13902  sinmpi  13903  cosmpi  13904  sinppi  13905  cosppi  13906  sincosq4sgn  13917  tangtx  13926  sincos4thpi  13928  sincos6thpi  13930  sincos3rdpi  13931  abssinper  13934  cosq34lt1  13938  1cxp  13988  ecxp  13989  rpcxpsqrt  14009  rpelogb  14034  2logb9irrALT  14059  binom4  14064  lgslem1  14068  lgsdir2lem1  14096  lgsdir2lem2  14097  lgsdir2lem3  14098  lgsdir2lem5  14100  lgs1  14112  2sqlem8  14126  ex-exp  14135  ex-bc  14137  ex-gcd  14139  cvgcmp2nlemabs  14436