Theorem oveq2i 5933

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

Syntax hints:   = wceq 1364  (class class class)co 5922

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  caov32  6111  oa1suc  6525  nnm1  6583  nnm2  6584  mapsnconst  6753  mapsncnv  6754  exmidpw2en  6973  mulidnq  7456  halfnqq  7477  addpinq1  7531  addnqpr1  7629  caucvgprlemm  7735  caucvgprprlemval  7755  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemaddq  7775  caucvgprprlem1  7776  caucvgprprlem2  7777  m1p1sr  7827  m1m1sr  7828  0idsr  7834  1idsr  7835  00sr  7836  pn0sr  7838  ltm1sr  7844  caucvgsrlemoffres  7867  caucvgsr  7869  mulresr  7905  pitonnlem2  7914  axi2m1  7942  ax1rid  7944  axcnre  7948  add42i  8192  negid  8273  negsub  8274  subneg  8275  negsubdii  8311  apreap  8614  recexaplem2  8679  muleqadd  8695  crap0  8985  2p2e4  9117  3p2e5  9132  3p3e6  9133  4p2e6  9134  4p3e7  9135  4p4e8  9136  5p2e7  9137  5p3e8  9138  5p4e9  9139  6p2e8  9140  6p3e9  9141  7p2e9  9142  3t3e9  9148  8th4div3  9210  halfpm6th  9211  iap0  9214  addltmul  9228  div4p1lem1div2  9245  peano2z  9362  nn0n0n1ge2  9396  nneoor  9428  zeo  9431  numsuc  9470  numltc  9482  numsucc  9496  numma  9500  nummul1c  9505  decrmac  9514  decsubi  9519  decmul1  9520  decmul10add  9525  6p5lem  9526  5p5e10  9527  6p4e10  9528  7p3e10  9531  8p2e10  9536  4t3lem  9553  9t11e99  9586  decbin2  9597  fztp  10153  fzprval  10157  fztpval  10158  fzshftral  10183  fz0tp  10197  fz0to3un2pr  10198  fzo01  10292  fzo12sn  10293  fzo0to2pr  10294  fzo0to3tp  10295  fzo0to42pr  10296  intqfrac2  10411  intfracq  10412  xnn0nnen  10529  sqval  10689  sq4e2t8  10729  cu2  10730  i3  10733  i4  10734  binom2i  10740  binom3  10749  3dec  10806  faclbnd  10833  faclbnd2  10834  bcn1  10850  bcn2  10856  4bc3eq4  10865  4bc2eq6  10866  reim0  11026  cji  11067  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemcalc3  11181  absi  11224  fsump1i  11598  fsumconst  11619  modfsummodlemstep  11622  arisum2  11664  geoihalfsum  11687  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  fprodconst  11785  fprodrec  11794  ef0lem  11825  ege2le3  11836  eft0val  11858  ef4p  11859  efgt1p2  11860  efgt1p  11861  tanval2ap  11878  efival  11897  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  3dvdsdec  12030  3dvds2dec  12031  odd2np1lem  12037  odd2np1  12038  oddp1even  12041  mod2eq1n2dvds  12044  opoe  12060  bits0  12112  6gcd4e2  12162  lcmneg  12242  3lcm2e6woprm  12254  6lcm4e12  12255  3prm  12296  3lcm2e6  12328  sqrt2irrlem  12329  pw2dvdslemn  12333  phiprm  12391  prmdiv  12403  pythagtriplem12  12444  pythagtriplem14  12446  pcfac  12519  prmpwdvds  12524  pockthi  12527  4sqlem5  12551  4sqlem13m  12572  modxai  12585  gcdi  12589  numexpp1  12593  numexp2x  12594  decsplit0b  12595  decsplit1  12597  decsplit  12598  2exp5  12601  2exp7  12603  2exp11  12605  2exp16  12606  ressval2  12744  ecqusaddd  13368  gsumfzconstf  13472  znbas  14200  znzrh2  14202  restin  14412  uptx  14510  cnrehmeocntop  14846  hoverb  14884  dvexp  14947  dvmptidcn  14950  dvmptccn  14951  dvmptid  14952  dvmptc  14953  dvmptfsum  14961  dveflem  14962  plymullem1  14984  sinhalfpilem  15027  efhalfpi  15035  cospi  15036  efipi  15037  sin2pi  15039  cos2pi  15040  ef2pi  15041  sin2pim  15049  cos2pim  15050  sinmpi  15051  cosmpi  15052  sinppi  15053  cosppi  15054  sincosq4sgn  15065  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  abssinper  15082  cosq34lt1  15086  1cxp  15136  ecxp  15137  rpcxpsqrt  15158  rpelogb  15185  2logb9irrALT  15210  binom4  15215  1sgmprm  15230  lgslem1  15241  lgsdir2lem1  15269  lgsdir2lem2  15270  lgsdir2lem3  15271  lgsdir2lem5  15273  lgs1  15285  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  gausslemma2dlem4  15305  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem3  15313  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  m1lgs  15326  2lgslem1a2  15328  2sqlem8  15364  ex-exp  15373  ex-bc  15375  ex-gcd  15377  cvgcmp2nlemabs  15676