Theorem oveq2i 5902

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 5899	. 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 1364  (class class class)co 5891

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5193  df-fv 5239  df-ov 5894

This theorem is referenced by:  caov32  6079  oa1suc  6486  nnm1  6544  nnm2  6545  mapsnconst  6712  mapsncnv  6713  mulidnq  7406  halfnqq  7427  addpinq1  7481  addnqpr1  7579  caucvgprlemm  7685  caucvgprprlemval  7705  caucvgprprlemnbj  7710  caucvgprprlemmu  7712  caucvgprprlemaddq  7725  caucvgprprlem1  7726  caucvgprprlem2  7727  m1p1sr  7777  m1m1sr  7778  0idsr  7784  1idsr  7785  00sr  7786  pn0sr  7788  ltm1sr  7794  caucvgsrlemoffres  7817  caucvgsr  7819  mulresr  7855  pitonnlem2  7864  axi2m1  7892  ax1rid  7894  axcnre  7898  add42i  8141  negid  8222  negsub  8223  subneg  8224  negsubdii  8260  apreap  8562  recexaplem2  8627  muleqadd  8643  crap0  8933  2p2e4  9064  3p2e5  9078  3p3e6  9079  4p2e6  9080  4p3e7  9081  4p4e8  9082  5p2e7  9083  5p3e8  9084  5p4e9  9085  6p2e8  9086  6p3e9  9087  7p2e9  9088  3t3e9  9094  8th4div3  9156  halfpm6th  9157  iap0  9160  addltmul  9173  div4p1lem1div2  9190  peano2z  9307  nn0n0n1ge2  9341  nneoor  9373  zeo  9376  numsuc  9415  numltc  9427  numsucc  9441  numma  9445  nummul1c  9450  decrmac  9459  decsubi  9464  decmul1  9465  decmul10add  9470  6p5lem  9471  5p5e10  9472  6p4e10  9473  7p3e10  9476  8p2e10  9481  4t3lem  9498  9t11e99  9531  decbin2  9542  fztp  10096  fzprval  10100  fztpval  10101  fzshftral  10126  fz0tp  10140  fz0to3un2pr  10141  fzo01  10234  fzo12sn  10235  fzo0to2pr  10236  fzo0to3tp  10237  fzo0to42pr  10238  intqfrac2  10337  intfracq  10338  sqval  10596  sq4e2t8  10636  cu2  10637  i3  10640  i4  10641  binom2i  10647  binom3  10656  3dec  10712  faclbnd  10739  faclbnd2  10740  bcn1  10756  bcn2  10762  4bc3eq4  10771  4bc2eq6  10772  reim0  10888  cji  10929  resqrexlemover  11037  resqrexlemcalc1  11041  resqrexlemcalc3  11043  absi  11086  fsump1i  11459  fsumconst  11480  modfsummodlemstep  11483  arisum2  11525  geoihalfsum  11548  mertenslemi1  11561  mertenslem2  11562  mertensabs  11563  fprodconst  11646  fprodrec  11655  ef0lem  11686  ege2le3  11697  eft0val  11719  ef4p  11720  efgt1p2  11721  efgt1p  11722  tanval2ap  11739  efival  11758  ef01bndlem  11782  sin01bnd  11783  cos01bnd  11784  cos1bnd  11785  cos2bnd  11786  3dvdsdec  11888  3dvds2dec  11889  odd2np1lem  11895  odd2np1  11896  oddp1even  11899  mod2eq1n2dvds  11902  opoe  11918  6gcd4e2  12014  lcmneg  12092  3lcm2e6woprm  12104  6lcm4e12  12105  3prm  12146  3lcm2e6  12178  sqrt2irrlem  12179  pw2dvdslemn  12183  phiprm  12241  prmdiv  12253  pythagtriplem12  12293  pythagtriplem14  12295  pcfac  12366  prmpwdvds  12371  pockthi  12374  4sqlem5  12398  ressval2  12544  restin  14060  uptx  14158  cnrehmeocntop  14477  dvexp  14559  dvmptidcn  14562  dvmptccn  14563  dveflem  14571  sinhalfpilem  14596  efhalfpi  14604  cospi  14605  efipi  14606  sin2pi  14608  cos2pi  14609  ef2pi  14610  sin2pim  14618  cos2pim  14619  sinmpi  14620  cosmpi  14621  sinppi  14622  cosppi  14623  sincosq4sgn  14634  tangtx  14643  sincos4thpi  14645  sincos6thpi  14647  sincos3rdpi  14648  abssinper  14651  cosq34lt1  14655  1cxp  14705  ecxp  14706  rpcxpsqrt  14726  rpelogb  14751  2logb9irrALT  14776  binom4  14781  lgslem1  14785  lgsdir2lem1  14813  lgsdir2lem2  14814  lgsdir2lem3  14815  lgsdir2lem5  14817  lgs1  14829  lgseisenlem1  14834  m1lgs  14836  2sqlem8  14854  ex-exp  14863  ex-bc  14865  ex-gcd  14867  cvgcmp2nlemabs  15165