Theorem oveq2i 6032

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq2i	⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 6029	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1397  (class class class)co 6021

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 6024

This theorem is referenced by:  caov32  6213  oa1suc  6638  nnm1  6696  nnm2  6697  mapsnconst  6866  mapsncnv  6867  exmidpw2en  7107  mulidnq  7612  halfnqq  7633  addpinq1  7687  addnqpr1  7785  caucvgprlemm  7891  caucvgprprlemval  7911  caucvgprprlemnbj  7916  caucvgprprlemmu  7918  caucvgprprlemaddq  7931  caucvgprprlem1  7932  caucvgprprlem2  7933  m1p1sr  7983  m1m1sr  7984  0idsr  7990  1idsr  7991  00sr  7992  pn0sr  7994  ltm1sr  8000  caucvgsrlemoffres  8023  caucvgsr  8025  mulresr  8061  pitonnlem2  8070  axi2m1  8098  ax1rid  8100  axcnre  8104  add42i  8348  negid  8429  negsub  8430  subneg  8431  negsubdii  8467  apreap  8770  recexaplem2  8835  muleqadd  8851  crap0  9141  2p2e4  9273  3p2e5  9288  3p3e6  9289  4p2e6  9290  4p3e7  9291  4p4e8  9292  5p2e7  9293  5p3e8  9294  5p4e9  9295  6p2e8  9296  6p3e9  9297  7p2e9  9298  3t3e9  9304  8th4div3  9366  halfpm6th  9367  iap0  9370  addltmul  9384  div4p1lem1div2  9401  peano2z  9518  nn0n0n1ge2  9553  nneoor  9585  zeo  9588  numsuc  9627  numltc  9639  numsucc  9653  numma  9657  nummul1c  9662  decrmac  9671  decsubi  9676  decmul1  9677  decmul10add  9682  6p5lem  9683  5p5e10  9684  6p4e10  9685  7p3e10  9688  8p2e10  9693  4t3lem  9710  9t11e99  9743  decbin2  9754  fztp  10316  fzprval  10320  fztpval  10321  fzshftral  10346  fz0tp  10360  fz0to3un2pr  10361  fzo01  10465  fzo12sn  10466  fzo0to2pr  10467  fzo0to3tp  10468  fzo0to42pr  10469  intqfrac2  10585  intfracq  10586  xnn0nnen  10703  sqval  10863  sq4e2t8  10903  cu2  10904  i3  10907  i4  10908  binom2i  10914  binom3  10923  3dec  10980  faclbnd  11007  faclbnd2  11008  bcn1  11024  bcn2  11030  4bc3eq4  11039  4bc2eq6  11040  ccatlid  11190  ccatrid  11191  pfx1  11291  pfxccatin12lem3  11320  pfxccatpfx1  11324  pfxccatpfx2  11325  cats1fvn  11352  cats1catd  11356  cats2catd  11357  reim0  11442  cji  11483  resqrexlemover  11591  resqrexlemcalc1  11595  resqrexlemcalc3  11597  absi  11640  fsump1i  12015  fsumconst  12036  modfsummodlemstep  12039  arisum2  12081  geoihalfsum  12104  mertenslemi1  12117  mertenslem2  12118  mertensabs  12119  fprodconst  12202  fprodrec  12211  ef0lem  12242  ege2le3  12253  eft0val  12275  ef4p  12276  efgt1p2  12277  efgt1p  12278  tanval2ap  12295  efival  12314  ef01bndlem  12338  sin01bnd  12339  cos01bnd  12340  cos1bnd  12341  cos2bnd  12342  3dvdsdec  12447  3dvds2dec  12448  odd2np1lem  12454  odd2np1  12455  oddp1even  12458  mod2eq1n2dvds  12461  opoe  12477  bits0  12530  0bits  12541  6gcd4e2  12587  lcmneg  12667  3lcm2e6woprm  12679  6lcm4e12  12680  3prm  12721  3lcm2e6  12753  sqrt2irrlem  12754  pw2dvdslemn  12758  phiprm  12816  prmdiv  12828  pythagtriplem12  12869  pythagtriplem14  12871  pcfac  12944  prmpwdvds  12949  pockthi  12952  4sqlem5  12976  4sqlem13m  12997  modxai  13010  gcdi  13014  numexpp1  13018  numexp2x  13019  decsplit0b  13020  decsplit1  13022  decsplit  13023  2exp5  13026  2exp7  13028  2exp11  13030  2exp16  13031  ressval2  13170  ecqusaddd  13846  gsumfzconstf  13950  znbas  14680  znzrh2  14682  restin  14927  uptx  15025  cnrehmeocntop  15361  hoverb  15399  dvexp  15462  dvmptidcn  15465  dvmptccn  15466  dvmptid  15467  dvmptc  15468  dvmptfsum  15476  dveflem  15477  plymullem1  15499  sinhalfpilem  15542  efhalfpi  15550  cospi  15551  efipi  15552  sin2pi  15554  cos2pi  15555  ef2pi  15556  sin2pim  15564  cos2pim  15565  sinmpi  15566  cosmpi  15567  sinppi  15568  cosppi  15569  sincosq4sgn  15580  tangtx  15589  sincos4thpi  15591  sincos6thpi  15593  sincos3rdpi  15594  abssinper  15597  cosq34lt1  15601  1cxp  15651  ecxp  15652  rpcxpsqrt  15673  rpelogb  15700  2logb9irrALT  15725  binom4  15730  1sgmprm  15745  lgslem1  15756  lgsdir2lem1  15784  lgsdir2lem2  15785  lgsdir2lem3  15786  lgsdir2lem5  15788  lgs1  15800  gausslemma2dlem1a  15814  gausslemma2dlem3  15819  gausslemma2dlem4  15820  gausslemma2d  15825  lgseisenlem1  15826  lgseisenlem3  15828  lgsquadlem1  15833  lgsquadlem2  15834  lgsquad2lem2  15838  m1lgs  15841  2lgslem1a2  15843  2sqlem8  15879  setsiedg  15930  vdegp1cid  16194  clwwlknonex2lem1  16315  ex-exp  16378  ex-bc  16380  ex-gcd  16382  cvgcmp2nlemabs  16695  gfsumcl  16747