Theorem oveq2i 5957

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 5954	. 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 1373  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  caov32  6136  oa1suc  6555  nnm1  6613  nnm2  6614  mapsnconst  6783  mapsncnv  6784  exmidpw2en  7011  mulidnq  7504  halfnqq  7525  addpinq1  7579  addnqpr1  7677  caucvgprlemm  7783  caucvgprprlemval  7803  caucvgprprlemnbj  7808  caucvgprprlemmu  7810  caucvgprprlemaddq  7823  caucvgprprlem1  7824  caucvgprprlem2  7825  m1p1sr  7875  m1m1sr  7876  0idsr  7882  1idsr  7883  00sr  7884  pn0sr  7886  ltm1sr  7892  caucvgsrlemoffres  7915  caucvgsr  7917  mulresr  7953  pitonnlem2  7962  axi2m1  7990  ax1rid  7992  axcnre  7996  add42i  8240  negid  8321  negsub  8322  subneg  8323  negsubdii  8359  apreap  8662  recexaplem2  8727  muleqadd  8743  crap0  9033  2p2e4  9165  3p2e5  9180  3p3e6  9181  4p2e6  9182  4p3e7  9183  4p4e8  9184  5p2e7  9185  5p3e8  9186  5p4e9  9187  6p2e8  9188  6p3e9  9189  7p2e9  9190  3t3e9  9196  8th4div3  9258  halfpm6th  9259  iap0  9262  addltmul  9276  div4p1lem1div2  9293  peano2z  9410  nn0n0n1ge2  9445  nneoor  9477  zeo  9480  numsuc  9519  numltc  9531  numsucc  9545  numma  9549  nummul1c  9554  decrmac  9563  decsubi  9568  decmul1  9569  decmul10add  9574  6p5lem  9575  5p5e10  9576  6p4e10  9577  7p3e10  9580  8p2e10  9585  4t3lem  9602  9t11e99  9635  decbin2  9646  fztp  10202  fzprval  10206  fztpval  10207  fzshftral  10232  fz0tp  10246  fz0to3un2pr  10247  fzo01  10347  fzo12sn  10348  fzo0to2pr  10349  fzo0to3tp  10350  fzo0to42pr  10351  intqfrac2  10466  intfracq  10467  xnn0nnen  10584  sqval  10744  sq4e2t8  10784  cu2  10785  i3  10788  i4  10789  binom2i  10795  binom3  10804  3dec  10861  faclbnd  10888  faclbnd2  10889  bcn1  10905  bcn2  10911  4bc3eq4  10920  4bc2eq6  10921  ccatlid  11065  ccatrid  11066  pfx1  11157  reim0  11205  cji  11246  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemcalc3  11360  absi  11403  fsump1i  11777  fsumconst  11798  modfsummodlemstep  11801  arisum2  11843  geoihalfsum  11866  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  fprodconst  11964  fprodrec  11973  ef0lem  12004  ege2le3  12015  eft0val  12037  ef4p  12038  efgt1p2  12039  efgt1p  12040  tanval2ap  12057  efival  12076  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  cos1bnd  12103  cos2bnd  12104  3dvdsdec  12209  3dvds2dec  12210  odd2np1lem  12216  odd2np1  12217  oddp1even  12220  mod2eq1n2dvds  12223  opoe  12239  bits0  12292  0bits  12303  6gcd4e2  12349  lcmneg  12429  3lcm2e6woprm  12441  6lcm4e12  12442  3prm  12483  3lcm2e6  12515  sqrt2irrlem  12516  pw2dvdslemn  12520  phiprm  12578  prmdiv  12590  pythagtriplem12  12631  pythagtriplem14  12633  pcfac  12706  prmpwdvds  12711  pockthi  12714  4sqlem5  12738  4sqlem13m  12759  modxai  12772  gcdi  12776  numexpp1  12780  numexp2x  12781  decsplit0b  12782  decsplit1  12784  decsplit  12785  2exp5  12788  2exp7  12790  2exp11  12792  2exp16  12793  ressval2  12931  ecqusaddd  13607  gsumfzconstf  13711  znbas  14439  znzrh2  14441  restin  14681  uptx  14779  cnrehmeocntop  15115  hoverb  15153  dvexp  15216  dvmptidcn  15219  dvmptccn  15220  dvmptid  15221  dvmptc  15222  dvmptfsum  15230  dveflem  15231  plymullem1  15253  sinhalfpilem  15296  efhalfpi  15304  cospi  15305  efipi  15306  sin2pi  15308  cos2pi  15309  ef2pi  15310  sin2pim  15318  cos2pim  15319  sinmpi  15320  cosmpi  15321  sinppi  15322  cosppi  15323  sincosq4sgn  15334  tangtx  15343  sincos4thpi  15345  sincos6thpi  15347  sincos3rdpi  15348  abssinper  15351  cosq34lt1  15355  1cxp  15405  ecxp  15406  rpcxpsqrt  15427  rpelogb  15454  2logb9irrALT  15479  binom4  15484  1sgmprm  15499  lgslem1  15510  lgsdir2lem1  15538  lgsdir2lem2  15539  lgsdir2lem3  15540  lgsdir2lem5  15542  lgs1  15554  gausslemma2dlem1a  15568  gausslemma2dlem3  15573  gausslemma2dlem4  15574  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem3  15582  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  m1lgs  15595  2lgslem1a2  15597  2sqlem8  15633  ex-exp  15700  ex-bc  15702  ex-gcd  15704  cvgcmp2nlemabs  16008