Theorem oveq2i 5885

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 5882	. 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 5874

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 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  caov32  6061  oa1suc  6467  nnm1  6525  nnm2  6526  mapsnconst  6693  mapsncnv  6694  mulidnq  7387  halfnqq  7408  addpinq1  7462  addnqpr1  7560  caucvgprlemm  7666  caucvgprprlemval  7686  caucvgprprlemnbj  7691  caucvgprprlemmu  7693  caucvgprprlemaddq  7706  caucvgprprlem1  7707  caucvgprprlem2  7708  m1p1sr  7758  m1m1sr  7759  0idsr  7765  1idsr  7766  00sr  7767  pn0sr  7769  ltm1sr  7775  caucvgsrlemoffres  7798  caucvgsr  7800  mulresr  7836  pitonnlem2  7845  axi2m1  7873  ax1rid  7875  axcnre  7879  add42i  8122  negid  8203  negsub  8204  subneg  8205  negsubdii  8241  apreap  8543  recexaplem2  8608  muleqadd  8624  crap0  8914  2p2e4  9045  3p2e5  9059  3p3e6  9060  4p2e6  9061  4p3e7  9062  4p4e8  9063  5p2e7  9064  5p3e8  9065  5p4e9  9066  6p2e8  9067  6p3e9  9068  7p2e9  9069  3t3e9  9075  8th4div3  9137  halfpm6th  9138  iap0  9141  addltmul  9154  div4p1lem1div2  9171  peano2z  9288  nn0n0n1ge2  9322  nneoor  9354  zeo  9357  numsuc  9396  numltc  9408  numsucc  9422  numma  9426  nummul1c  9431  decrmac  9440  decsubi  9445  decmul1  9446  decmul10add  9451  6p5lem  9452  5p5e10  9453  6p4e10  9454  7p3e10  9457  8p2e10  9462  4t3lem  9479  9t11e99  9512  decbin2  9523  fztp  10077  fzprval  10081  fztpval  10082  fzshftral  10107  fz0tp  10121  fz0to3un2pr  10122  fzo01  10215  fzo12sn  10216  fzo0to2pr  10217  fzo0to3tp  10218  fzo0to42pr  10219  intqfrac2  10318  intfracq  10319  sqval  10577  sq4e2t8  10617  cu2  10618  i3  10621  i4  10622  binom2i  10628  binom3  10637  3dec  10693  faclbnd  10720  faclbnd2  10721  bcn1  10737  bcn2  10743  4bc3eq4  10752  4bc2eq6  10753  reim0  10869  cji  10910  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemcalc3  11024  absi  11067  fsump1i  11440  fsumconst  11461  modfsummodlemstep  11464  arisum2  11506  geoihalfsum  11529  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  fprodconst  11627  fprodrec  11636  ef0lem  11667  ege2le3  11678  eft0val  11700  ef4p  11701  efgt1p2  11702  efgt1p  11703  tanval2ap  11720  efival  11739  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  3dvdsdec  11869  3dvds2dec  11870  odd2np1lem  11876  odd2np1  11877  oddp1even  11880  mod2eq1n2dvds  11883  opoe  11899  6gcd4e2  11995  lcmneg  12073  3lcm2e6woprm  12085  6lcm4e12  12086  3prm  12127  3lcm2e6  12159  sqrt2irrlem  12160  pw2dvdslemn  12164  phiprm  12222  prmdiv  12234  pythagtriplem12  12274  pythagtriplem14  12276  pcfac  12347  prmpwdvds  12352  pockthi  12355  4sqlem5  12379  ressval2  12525  restin  13646  uptx  13744  cnrehmeocntop  14063  dvexp  14145  dvmptidcn  14148  dvmptccn  14149  dveflem  14157  sinhalfpilem  14182  efhalfpi  14190  cospi  14191  efipi  14192  sin2pi  14194  cos2pi  14195  ef2pi  14196  sin2pim  14204  cos2pim  14205  sinmpi  14206  cosmpi  14207  sinppi  14208  cosppi  14209  sincosq4sgn  14220  tangtx  14229  sincos4thpi  14231  sincos6thpi  14233  sincos3rdpi  14234  abssinper  14237  cosq34lt1  14241  1cxp  14291  ecxp  14292  rpcxpsqrt  14312  rpelogb  14337  2logb9irrALT  14362  binom4  14367  lgslem1  14371  lgsdir2lem1  14399  lgsdir2lem2  14400  lgsdir2lem3  14401  lgsdir2lem5  14403  lgs1  14415  lgseisenlem1  14420  m1lgs  14422  2sqlem8  14440  ex-exp  14449  ex-bc  14451  ex-gcd  14453  cvgcmp2nlemabs  14750