Theorem oveq2i 5955

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

Syntax hints:   = wceq 1373  (class class class)co 5944

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  caov32  6134  oa1suc  6553  nnm1  6611  nnm2  6612  mapsnconst  6781  mapsncnv  6782  exmidpw2en  7009  mulidnq  7502  halfnqq  7523  addpinq1  7577  addnqpr1  7675  caucvgprlemm  7781  caucvgprprlemval  7801  caucvgprprlemnbj  7806  caucvgprprlemmu  7808  caucvgprprlemaddq  7821  caucvgprprlem1  7822  caucvgprprlem2  7823  m1p1sr  7873  m1m1sr  7874  0idsr  7880  1idsr  7881  00sr  7882  pn0sr  7884  ltm1sr  7890  caucvgsrlemoffres  7913  caucvgsr  7915  mulresr  7951  pitonnlem2  7960  axi2m1  7988  ax1rid  7990  axcnre  7994  add42i  8238  negid  8319  negsub  8320  subneg  8321  negsubdii  8357  apreap  8660  recexaplem2  8725  muleqadd  8741  crap0  9031  2p2e4  9163  3p2e5  9178  3p3e6  9179  4p2e6  9180  4p3e7  9181  4p4e8  9182  5p2e7  9183  5p3e8  9184  5p4e9  9185  6p2e8  9186  6p3e9  9187  7p2e9  9188  3t3e9  9194  8th4div3  9256  halfpm6th  9257  iap0  9260  addltmul  9274  div4p1lem1div2  9291  peano2z  9408  nn0n0n1ge2  9443  nneoor  9475  zeo  9478  numsuc  9517  numltc  9529  numsucc  9543  numma  9547  nummul1c  9552  decrmac  9561  decsubi  9566  decmul1  9567  decmul10add  9572  6p5lem  9573  5p5e10  9574  6p4e10  9575  7p3e10  9578  8p2e10  9583  4t3lem  9600  9t11e99  9633  decbin2  9644  fztp  10200  fzprval  10204  fztpval  10205  fzshftral  10230  fz0tp  10244  fz0to3un2pr  10245  fzo01  10345  fzo12sn  10346  fzo0to2pr  10347  fzo0to3tp  10348  fzo0to42pr  10349  intqfrac2  10464  intfracq  10465  xnn0nnen  10582  sqval  10742  sq4e2t8  10782  cu2  10783  i3  10786  i4  10787  binom2i  10793  binom3  10802  3dec  10859  faclbnd  10886  faclbnd2  10887  bcn1  10903  bcn2  10909  4bc3eq4  10918  4bc2eq6  10919  ccatlid  11062  ccatrid  11063  reim0  11172  cji  11213  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemcalc3  11327  absi  11370  fsump1i  11744  fsumconst  11765  modfsummodlemstep  11768  arisum2  11810  geoihalfsum  11833  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  fprodconst  11931  fprodrec  11940  ef0lem  11971  ege2le3  11982  eft0val  12004  ef4p  12005  efgt1p2  12006  efgt1p  12007  tanval2ap  12024  efival  12043  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos1bnd  12070  cos2bnd  12071  3dvdsdec  12176  3dvds2dec  12177  odd2np1lem  12183  odd2np1  12184  oddp1even  12187  mod2eq1n2dvds  12190  opoe  12206  bits0  12259  0bits  12270  6gcd4e2  12316  lcmneg  12396  3lcm2e6woprm  12408  6lcm4e12  12409  3prm  12450  3lcm2e6  12482  sqrt2irrlem  12483  pw2dvdslemn  12487  phiprm  12545  prmdiv  12557  pythagtriplem12  12598  pythagtriplem14  12600  pcfac  12673  prmpwdvds  12678  pockthi  12681  4sqlem5  12705  4sqlem13m  12726  modxai  12739  gcdi  12743  numexpp1  12747  numexp2x  12748  decsplit0b  12749  decsplit1  12751  decsplit  12752  2exp5  12755  2exp7  12757  2exp11  12759  2exp16  12760  ressval2  12898  ecqusaddd  13574  gsumfzconstf  13678  znbas  14406  znzrh2  14408  restin  14648  uptx  14746  cnrehmeocntop  15082  hoverb  15120  dvexp  15183  dvmptidcn  15186  dvmptccn  15187  dvmptid  15188  dvmptc  15189  dvmptfsum  15197  dveflem  15198  plymullem1  15220  sinhalfpilem  15263  efhalfpi  15271  cospi  15272  efipi  15273  sin2pi  15275  cos2pi  15276  ef2pi  15277  sin2pim  15285  cos2pim  15286  sinmpi  15287  cosmpi  15288  sinppi  15289  cosppi  15290  sincosq4sgn  15301  tangtx  15310  sincos4thpi  15312  sincos6thpi  15314  sincos3rdpi  15315  abssinper  15318  cosq34lt1  15322  1cxp  15372  ecxp  15373  rpcxpsqrt  15394  rpelogb  15421  2logb9irrALT  15446  binom4  15451  1sgmprm  15466  lgslem1  15477  lgsdir2lem1  15505  lgsdir2lem2  15506  lgsdir2lem3  15507  lgsdir2lem5  15509  lgs1  15521  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  gausslemma2dlem4  15541  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem3  15549  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  m1lgs  15562  2lgslem1a2  15564  2sqlem8  15600  ex-exp  15663  ex-bc  15665  ex-gcd  15667  cvgcmp2nlemabs  15971