Theorem oveq2i 5543

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 5540	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	ax-mp 7	1 |- ( C F A ) = ( C F B )

Syntax hints:   = wceq 1284  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  caov32  5708  oa1suc  6070  nnm1  6120  nnm2  6121  mulidnq  6579  halfnqq  6600  addpinq1  6654  addnqpr1  6752  caucvgprlemm  6858  caucvgprprlemval  6878  caucvgprprlemnbj  6883  caucvgprprlemmu  6885  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  m1p1sr  6937  m1m1sr  6938  0idsr  6944  1idsr  6945  00sr  6946  pn0sr  6948  caucvgsrlemoffres  6976  caucvgsr  6978  mulresr  7006  pitonnlem2  7015  axi2m1  7041  ax1rid  7043  axcnre  7047  add42i  7274  negid  7355  negsub  7356  subneg  7357  negsubdii  7393  apreap  7687  recexaplem2  7742  muleqadd  7758  crap0  8035  2p2e4  8159  3p2e5  8173  3p3e6  8174  4p2e6  8175  4p3e7  8176  4p4e8  8177  5p2e7  8178  5p3e8  8179  5p4e9  8180  6p2e8  8181  6p3e9  8182  7p2e9  8183  3t3e9  8189  8th4div3  8250  halfpm6th  8251  iap0  8254  addltmul  8267  div4p1lem1div2  8284  peano2z  8387  nn0n0n1ge2  8418  nneoor  8449  zeo  8452  numsuc  8490  numltc  8502  numsucc  8516  numma  8520  nummul1c  8525  decrmac  8534  decsubi  8539  decmul1  8540  decmul10add  8545  6p5lem  8546  5p5e10  8547  6p4e10  8548  7p3e10  8551  8p2e10  8556  4t3lem  8573  9t11e99  8606  decbin2  8617  fztp  9095  fzprval  9099  fztpval  9100  fzshftral  9125  fz0tp  9135  fzo01  9225  fzo12sn  9226  fzo0to2pr  9227  fzo0to3tp  9228  fzo0to42pr  9229  intqfrac2  9321  intfracq  9322  sqval  9534  cu2  9573  i3  9576  i4  9577  binom2i  9583  binom3  9590  3dec  9642  faclbnd  9668  faclbnd2  9669  bcn1  9685  bcn2  9691  4bc3eq4  9700  4bc2eq6  9701  reim0  9748  cji  9789  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemcalc3  9902  absi  9945  3dvdsdec  10264  3dvds2dec  10265  odd2np1lem  10271  odd2np1  10272  oddp1even  10275  mod2eq1n2dvds  10279  opoe  10295  6gcd4e2  10384  lcmneg  10456  3lcm2e6woprm  10468  6lcm4e12  10469  3prm  10510  3lcm2e6  10539  sqrt2irrlem  10540  pw2dvdslemn  10543  ex-bc  10566  ex-gcd  10568