Theorem oveq2i 6028

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

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

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 6020

This theorem is referenced by:  caov32  6209  oa1suc  6634  nnm1  6692  nnm2  6693  mapsnconst  6862  mapsncnv  6863  exmidpw2en  7103  mulidnq  7608  halfnqq  7629  addpinq1  7683  addnqpr1  7781  caucvgprlemm  7887  caucvgprprlemval  7907  caucvgprprlemnbj  7912  caucvgprprlemmu  7914  caucvgprprlemaddq  7927  caucvgprprlem1  7928  caucvgprprlem2  7929  m1p1sr  7979  m1m1sr  7980  0idsr  7986  1idsr  7987  00sr  7988  pn0sr  7990  ltm1sr  7996  caucvgsrlemoffres  8019  caucvgsr  8021  mulresr  8057  pitonnlem2  8066  axi2m1  8094  ax1rid  8096  axcnre  8100  add42i  8344  negid  8425  negsub  8426  subneg  8427  negsubdii  8463  apreap  8766  recexaplem2  8831  muleqadd  8847  crap0  9137  2p2e4  9269  3p2e5  9284  3p3e6  9285  4p2e6  9286  4p3e7  9287  4p4e8  9288  5p2e7  9289  5p3e8  9290  5p4e9  9291  6p2e8  9292  6p3e9  9293  7p2e9  9294  3t3e9  9300  8th4div3  9362  halfpm6th  9363  iap0  9366  addltmul  9380  div4p1lem1div2  9397  peano2z  9514  nn0n0n1ge2  9549  nneoor  9581  zeo  9584  numsuc  9623  numltc  9635  numsucc  9649  numma  9653  nummul1c  9658  decrmac  9667  decsubi  9672  decmul1  9673  decmul10add  9678  6p5lem  9679  5p5e10  9680  6p4e10  9681  7p3e10  9684  8p2e10  9689  4t3lem  9706  9t11e99  9739  decbin2  9750  fztp  10312  fzprval  10316  fztpval  10317  fzshftral  10342  fz0tp  10356  fz0to3un2pr  10357  fzo01  10460  fzo12sn  10461  fzo0to2pr  10462  fzo0to3tp  10463  fzo0to42pr  10464  intqfrac2  10580  intfracq  10581  xnn0nnen  10698  sqval  10858  sq4e2t8  10898  cu2  10899  i3  10902  i4  10903  binom2i  10909  binom3  10918  3dec  10975  faclbnd  11002  faclbnd2  11003  bcn1  11019  bcn2  11025  4bc3eq4  11034  4bc2eq6  11035  ccatlid  11182  ccatrid  11183  pfx1  11283  pfxccatin12lem3  11312  pfxccatpfx1  11316  pfxccatpfx2  11317  cats1fvn  11344  cats1catd  11348  cats2catd  11349  reim0  11421  cji  11462  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemcalc3  11576  absi  11619  fsump1i  11993  fsumconst  12014  modfsummodlemstep  12017  arisum2  12059  geoihalfsum  12082  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  fprodconst  12180  fprodrec  12189  ef0lem  12220  ege2le3  12231  eft0val  12253  ef4p  12254  efgt1p2  12255  efgt1p  12256  tanval2ap  12273  efival  12292  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  3dvdsdec  12425  3dvds2dec  12426  odd2np1lem  12432  odd2np1  12433  oddp1even  12436  mod2eq1n2dvds  12439  opoe  12455  bits0  12508  0bits  12519  6gcd4e2  12565  lcmneg  12645  3lcm2e6woprm  12657  6lcm4e12  12658  3prm  12699  3lcm2e6  12731  sqrt2irrlem  12732  pw2dvdslemn  12736  phiprm  12794  prmdiv  12806  pythagtriplem12  12847  pythagtriplem14  12849  pcfac  12922  prmpwdvds  12927  pockthi  12930  4sqlem5  12954  4sqlem13m  12975  modxai  12988  gcdi  12992  numexpp1  12996  numexp2x  12997  decsplit0b  12998  decsplit1  13000  decsplit  13001  2exp5  13004  2exp7  13006  2exp11  13008  2exp16  13009  ressval2  13148  ecqusaddd  13824  gsumfzconstf  13928  znbas  14657  znzrh2  14659  restin  14899  uptx  14997  cnrehmeocntop  15333  hoverb  15371  dvexp  15434  dvmptidcn  15437  dvmptccn  15438  dvmptid  15439  dvmptc  15440  dvmptfsum  15448  dveflem  15449  plymullem1  15471  sinhalfpilem  15514  efhalfpi  15522  cospi  15523  efipi  15524  sin2pi  15526  cos2pi  15527  ef2pi  15528  sin2pim  15536  cos2pim  15537  sinmpi  15538  cosmpi  15539  sinppi  15540  cosppi  15541  sincosq4sgn  15552  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  sincos3rdpi  15566  abssinper  15569  cosq34lt1  15573  1cxp  15623  ecxp  15624  rpcxpsqrt  15645  rpelogb  15672  2logb9irrALT  15697  binom4  15702  1sgmprm  15717  lgslem1  15728  lgsdir2lem1  15756  lgsdir2lem2  15757  lgsdir2lem3  15758  lgsdir2lem5  15760  lgs1  15772  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  gausslemma2dlem4  15792  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem3  15800  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  m1lgs  15813  2lgslem1a2  15815  2sqlem8  15851  setsiedg  15902  vdegp1cid  16166  clwwlknonex2lem1  16287  ex-exp  16323  ex-bc  16325  ex-gcd  16327  cvgcmp2nlemabs  16636