Theorem oveq2i 5930

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  caov32  6108  oa1suc  6522  nnm1  6580  nnm2  6581  mapsnconst  6750  mapsncnv  6751  exmidpw2en  6970  mulidnq  7451  halfnqq  7472  addpinq1  7526  addnqpr1  7624  caucvgprlemm  7730  caucvgprprlemval  7750  caucvgprprlemnbj  7755  caucvgprprlemmu  7757  caucvgprprlemaddq  7770  caucvgprprlem1  7771  caucvgprprlem2  7772  m1p1sr  7822  m1m1sr  7823  0idsr  7829  1idsr  7830  00sr  7831  pn0sr  7833  ltm1sr  7839  caucvgsrlemoffres  7862  caucvgsr  7864  mulresr  7900  pitonnlem2  7909  axi2m1  7937  ax1rid  7939  axcnre  7943  add42i  8187  negid  8268  negsub  8269  subneg  8270  negsubdii  8306  apreap  8608  recexaplem2  8673  muleqadd  8689  crap0  8979  2p2e4  9111  3p2e5  9126  3p3e6  9127  4p2e6  9128  4p3e7  9129  4p4e8  9130  5p2e7  9131  5p3e8  9132  5p4e9  9133  6p2e8  9134  6p3e9  9135  7p2e9  9136  3t3e9  9142  8th4div3  9204  halfpm6th  9205  iap0  9208  addltmul  9222  div4p1lem1div2  9239  peano2z  9356  nn0n0n1ge2  9390  nneoor  9422  zeo  9425  numsuc  9464  numltc  9476  numsucc  9490  numma  9494  nummul1c  9499  decrmac  9508  decsubi  9513  decmul1  9514  decmul10add  9519  6p5lem  9520  5p5e10  9521  6p4e10  9522  7p3e10  9525  8p2e10  9530  4t3lem  9547  9t11e99  9580  decbin2  9591  fztp  10147  fzprval  10151  fztpval  10152  fzshftral  10177  fz0tp  10191  fz0to3un2pr  10192  fzo01  10286  fzo12sn  10287  fzo0to2pr  10288  fzo0to3tp  10289  fzo0to42pr  10290  intqfrac2  10393  intfracq  10394  xnn0nnen  10511  sqval  10671  sq4e2t8  10711  cu2  10712  i3  10715  i4  10716  binom2i  10722  binom3  10731  3dec  10788  faclbnd  10815  faclbnd2  10816  bcn1  10832  bcn2  10838  4bc3eq4  10847  4bc2eq6  10848  reim0  11008  cji  11049  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemcalc3  11163  absi  11206  fsump1i  11579  fsumconst  11600  modfsummodlemstep  11603  arisum2  11645  geoihalfsum  11668  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  fprodconst  11766  fprodrec  11775  ef0lem  11806  ege2le3  11817  eft0val  11839  ef4p  11840  efgt1p2  11841  efgt1p  11842  tanval2ap  11859  efival  11878  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  3dvdsdec  12009  3dvds2dec  12010  odd2np1lem  12016  odd2np1  12017  oddp1even  12020  mod2eq1n2dvds  12023  opoe  12039  6gcd4e2  12135  lcmneg  12215  3lcm2e6woprm  12227  6lcm4e12  12228  3prm  12269  3lcm2e6  12301  sqrt2irrlem  12302  pw2dvdslemn  12306  phiprm  12364  prmdiv  12376  pythagtriplem12  12416  pythagtriplem14  12418  pcfac  12491  prmpwdvds  12496  pockthi  12499  4sqlem5  12523  4sqlem13m  12544  ressval2  12687  ecqusaddd  13311  gsumfzconstf  13415  znbas  14143  znzrh2  14145  restin  14355  uptx  14453  cnrehmeocntop  14789  hoverb  14827  dvexp  14890  dvmptidcn  14893  dvmptccn  14894  dvmptid  14895  dvmptc  14896  dvmptfsum  14904  dveflem  14905  plymullem1  14927  sinhalfpilem  14967  efhalfpi  14975  cospi  14976  efipi  14977  sin2pi  14979  cos2pi  14980  ef2pi  14981  sin2pim  14989  cos2pim  14990  sinmpi  14991  cosmpi  14992  sinppi  14993  cosppi  14994  sincosq4sgn  15005  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  abssinper  15022  cosq34lt1  15026  1cxp  15076  ecxp  15077  rpcxpsqrt  15097  rpelogb  15122  2logb9irrALT  15147  binom4  15152  lgslem1  15157  lgsdir2lem1  15185  lgsdir2lem2  15186  lgsdir2lem3  15187  lgsdir2lem5  15189  lgs1  15201  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem3  15229  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  m1lgs  15242  2lgslem1a2  15244  2sqlem8  15280  ex-exp  15289  ex-bc  15291  ex-gcd  15293  cvgcmp2nlemabs  15592