Theorem oveq2i 6029

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 6026	. 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 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  caov32  6210  oa1suc  6635  nnm1  6693  nnm2  6694  mapsnconst  6863  mapsncnv  6864  exmidpw2en  7104  mulidnq  7609  halfnqq  7630  addpinq1  7684  addnqpr1  7782  caucvgprlemm  7888  caucvgprprlemval  7908  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  m1p1sr  7980  m1m1sr  7981  0idsr  7987  1idsr  7988  00sr  7989  pn0sr  7991  ltm1sr  7997  caucvgsrlemoffres  8020  caucvgsr  8022  mulresr  8058  pitonnlem2  8067  axi2m1  8095  ax1rid  8097  axcnre  8101  add42i  8345  negid  8426  negsub  8427  subneg  8428  negsubdii  8464  apreap  8767  recexaplem2  8832  muleqadd  8848  crap0  9138  2p2e4  9270  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  3t3e9  9301  8th4div3  9363  halfpm6th  9364  iap0  9367  addltmul  9381  div4p1lem1div2  9398  peano2z  9515  nn0n0n1ge2  9550  nneoor  9582  zeo  9585  numsuc  9624  numltc  9636  numsucc  9650  numma  9654  nummul1c  9659  decrmac  9668  decsubi  9673  decmul1  9674  decmul10add  9679  6p5lem  9680  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  4t3lem  9707  9t11e99  9740  decbin2  9751  fztp  10313  fzprval  10317  fztpval  10318  fzshftral  10343  fz0tp  10357  fz0to3un2pr  10358  fzo01  10462  fzo12sn  10463  fzo0to2pr  10464  fzo0to3tp  10465  fzo0to42pr  10466  intqfrac2  10582  intfracq  10583  xnn0nnen  10700  sqval  10860  sq4e2t8  10900  cu2  10901  i3  10904  i4  10905  binom2i  10911  binom3  10920  3dec  10977  faclbnd  11004  faclbnd2  11005  bcn1  11021  bcn2  11027  4bc3eq4  11036  4bc2eq6  11037  ccatlid  11187  ccatrid  11188  pfx1  11288  pfxccatin12lem3  11317  pfxccatpfx1  11321  pfxccatpfx2  11322  cats1fvn  11349  cats1catd  11353  cats2catd  11354  reim0  11439  cji  11480  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemcalc3  11594  absi  11637  fsump1i  12012  fsumconst  12033  modfsummodlemstep  12036  arisum2  12078  geoihalfsum  12101  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  fprodconst  12199  fprodrec  12208  ef0lem  12239  ege2le3  12250  eft0val  12272  ef4p  12273  efgt1p2  12274  efgt1p  12275  tanval2ap  12292  efival  12311  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  3dvdsdec  12444  3dvds2dec  12445  odd2np1lem  12451  odd2np1  12452  oddp1even  12455  mod2eq1n2dvds  12458  opoe  12474  bits0  12527  0bits  12538  6gcd4e2  12584  lcmneg  12664  3lcm2e6woprm  12676  6lcm4e12  12677  3prm  12718  3lcm2e6  12750  sqrt2irrlem  12751  pw2dvdslemn  12755  phiprm  12813  prmdiv  12825  pythagtriplem12  12866  pythagtriplem14  12868  pcfac  12941  prmpwdvds  12946  pockthi  12949  4sqlem5  12973  4sqlem13m  12994  modxai  13007  gcdi  13011  numexpp1  13015  numexp2x  13016  decsplit0b  13017  decsplit1  13019  decsplit  13020  2exp5  13023  2exp7  13025  2exp11  13027  2exp16  13028  ressval2  13167  ecqusaddd  13843  gsumfzconstf  13947  znbas  14677  znzrh2  14679  restin  14919  uptx  15017  cnrehmeocntop  15353  hoverb  15391  dvexp  15454  dvmptidcn  15457  dvmptccn  15458  dvmptid  15459  dvmptc  15460  dvmptfsum  15468  dveflem  15469  plymullem1  15491  sinhalfpilem  15534  efhalfpi  15542  cospi  15543  efipi  15544  sin2pi  15546  cos2pi  15547  ef2pi  15548  sin2pim  15556  cos2pim  15557  sinmpi  15558  cosmpi  15559  sinppi  15560  cosppi  15561  sincosq4sgn  15572  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  sincos3rdpi  15586  abssinper  15589  cosq34lt1  15593  1cxp  15643  ecxp  15644  rpcxpsqrt  15665  rpelogb  15692  2logb9irrALT  15717  binom4  15722  1sgmprm  15737  lgslem1  15748  lgsdir2lem1  15776  lgsdir2lem2  15777  lgsdir2lem3  15778  lgsdir2lem5  15780  lgs1  15792  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  gausslemma2dlem4  15812  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem3  15820  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  m1lgs  15833  2lgslem1a2  15835  2sqlem8  15871  setsiedg  15922  vdegp1cid  16186  clwwlknonex2lem1  16307  ex-exp  16370  ex-bc  16372  ex-gcd  16374  cvgcmp2nlemabs  16687  gfsumcl  16739