Theorem oveq2i 5645

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

Syntax hints:   = wceq 1289  (class class class)co 5634

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637

This theorem is referenced by:  caov32  5814  oa1suc  6210  nnm1  6263  nnm2  6264  mapsnconst  6431  mapsncnv  6432  mulidnq  6927  halfnqq  6948  addpinq1  7002  addnqpr1  7100  caucvgprlemm  7206  caucvgprprlemval  7226  caucvgprprlemnbj  7231  caucvgprprlemmu  7233  caucvgprprlemaddq  7246  caucvgprprlem1  7247  caucvgprprlem2  7248  m1p1sr  7285  m1m1sr  7286  0idsr  7292  1idsr  7293  00sr  7294  pn0sr  7296  caucvgsrlemoffres  7324  caucvgsr  7326  mulresr  7354  pitonnlem2  7363  axi2m1  7389  ax1rid  7391  axcnre  7395  add42i  7627  negid  7708  negsub  7709  subneg  7710  negsubdii  7746  apreap  8040  recexaplem2  8095  muleqadd  8111  crap0  8390  2p2e4  8513  3p2e5  8527  3p3e6  8528  4p2e6  8529  4p3e7  8530  4p4e8  8531  5p2e7  8532  5p3e8  8533  5p4e9  8534  6p2e8  8535  6p3e9  8536  7p2e9  8537  3t3e9  8543  8th4div3  8605  halfpm6th  8606  iap0  8609  addltmul  8622  div4p1lem1div2  8639  peano2z  8756  nn0n0n1ge2  8787  nneoor  8818  zeo  8821  numsuc  8859  numltc  8871  numsucc  8885  numma  8889  nummul1c  8894  decrmac  8903  decsubi  8908  decmul1  8909  decmul10add  8914  6p5lem  8915  5p5e10  8916  6p4e10  8917  7p3e10  8920  8p2e10  8925  4t3lem  8942  9t11e99  8975  decbin2  8986  fztp  9459  fzprval  9463  fztpval  9464  fzshftral  9489  fz0tp  9500  fzo01  9592  fzo12sn  9593  fzo0to2pr  9594  fzo0to3tp  9595  fzo0to42pr  9596  intqfrac2  9691  intfracq  9692  sqval  9978  sq4e2t8  10017  cu2  10018  i3  10021  i4  10022  binom2i  10028  binom3  10036  3dec  10088  faclbnd  10114  faclbnd2  10115  bcn1  10131  bcn2  10137  4bc3eq4  10146  4bc2eq6  10147  reim0  10260  cji  10301  resqrexlemover  10408  resqrexlemcalc1  10412  resqrexlemcalc3  10414  absi  10457  fsump1i  10790  fsumconst  10811  modfsummodlemstep  10814  arisum2  10854  geoihalfsum  10877  3dvdsdec  10958  3dvds2dec  10959  odd2np1lem  10965  odd2np1  10966  oddp1even  10969  mod2eq1n2dvds  10972  opoe  10988  6gcd4e2  11077  lcmneg  11149  3lcm2e6woprm  11161  6lcm4e12  11162  3prm  11203  3lcm2e6  11232  sqrt2irrlem  11233  pw2dvdslemn  11236  phiprm  11292  ex-exp  11311  ex-bc  11313  ex-gcd  11315