Theorem oveq2i 5853

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 5850	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1343  (class class class)co 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  caov32  6029  oa1suc  6435  nnm1  6492  nnm2  6493  mapsnconst  6660  mapsncnv  6661  mulidnq  7330  halfnqq  7351  addpinq1  7405  addnqpr1  7503  caucvgprlemm  7609  caucvgprprlemval  7629  caucvgprprlemnbj  7634  caucvgprprlemmu  7636  caucvgprprlemaddq  7649  caucvgprprlem1  7650  caucvgprprlem2  7651  m1p1sr  7701  m1m1sr  7702  0idsr  7708  1idsr  7709  00sr  7710  pn0sr  7712  ltm1sr  7718  caucvgsrlemoffres  7741  caucvgsr  7743  mulresr  7779  pitonnlem2  7788  axi2m1  7816  ax1rid  7818  axcnre  7822  add42i  8064  negid  8145  negsub  8146  subneg  8147  negsubdii  8183  apreap  8485  recexaplem2  8549  muleqadd  8565  crap0  8853  2p2e4  8984  3p2e5  8998  3p3e6  8999  4p2e6  9000  4p3e7  9001  4p4e8  9002  5p2e7  9003  5p3e8  9004  5p4e9  9005  6p2e8  9006  6p3e9  9007  7p2e9  9008  3t3e9  9014  8th4div3  9076  halfpm6th  9077  iap0  9080  addltmul  9093  div4p1lem1div2  9110  peano2z  9227  nn0n0n1ge2  9261  nneoor  9293  zeo  9296  numsuc  9335  numltc  9347  numsucc  9361  numma  9365  nummul1c  9370  decrmac  9379  decsubi  9384  decmul1  9385  decmul10add  9390  6p5lem  9391  5p5e10  9392  6p4e10  9393  7p3e10  9396  8p2e10  9401  4t3lem  9418  9t11e99  9451  decbin2  9462  fztp  10013  fzprval  10017  fztpval  10018  fzshftral  10043  fz0tp  10057  fz0to3un2pr  10058  fzo01  10151  fzo12sn  10152  fzo0to2pr  10153  fzo0to3tp  10154  fzo0to42pr  10155  intqfrac2  10254  intfracq  10255  sqval  10513  sq4e2t8  10552  cu2  10553  i3  10556  i4  10557  binom2i  10563  binom3  10572  3dec  10627  faclbnd  10654  faclbnd2  10655  bcn1  10671  bcn2  10677  4bc3eq4  10686  4bc2eq6  10687  reim0  10803  cji  10844  resqrexlemover  10952  resqrexlemcalc1  10956  resqrexlemcalc3  10958  absi  11001  fsump1i  11374  fsumconst  11395  modfsummodlemstep  11398  arisum2  11440  geoihalfsum  11463  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  fprodconst  11561  fprodrec  11570  ef0lem  11601  ege2le3  11612  eft0val  11634  ef4p  11635  efgt1p2  11636  efgt1p  11637  tanval2ap  11654  efival  11673  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  3dvdsdec  11802  3dvds2dec  11803  odd2np1lem  11809  odd2np1  11810  oddp1even  11813  mod2eq1n2dvds  11816  opoe  11832  6gcd4e2  11928  lcmneg  12006  3lcm2e6woprm  12018  6lcm4e12  12019  3prm  12060  3lcm2e6  12092  sqrt2irrlem  12093  pw2dvdslemn  12097  phiprm  12155  prmdiv  12167  pythagtriplem12  12207  pythagtriplem14  12209  pcfac  12280  prmpwdvds  12285  pockthi  12288  4sqlem5  12312  restin  12816  uptx  12914  cnrehmeocntop  13233  dvexp  13315  dvmptidcn  13318  dvmptccn  13319  dveflem  13327  sinhalfpilem  13352  efhalfpi  13360  cospi  13361  efipi  13362  sin2pi  13364  cos2pi  13365  ef2pi  13366  sin2pim  13374  cos2pim  13375  sinmpi  13376  cosmpi  13377  sinppi  13378  cosppi  13379  sincosq4sgn  13390  tangtx  13399  sincos4thpi  13401  sincos6thpi  13403  sincos3rdpi  13404  abssinper  13407  cosq34lt1  13411  1cxp  13461  ecxp  13462  rpcxpsqrt  13482  rpelogb  13507  2logb9irrALT  13532  binom4  13537  lgslem1  13541  lgsdir2lem1  13569  lgsdir2lem2  13570  lgsdir2lem3  13571  lgsdir2lem5  13573  lgs1  13585  2sqlem8  13599  ex-exp  13608  ex-bc  13610  ex-gcd  13612  cvgcmp2nlemabs  13911