Theorem oveq2i 5523

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

Syntax hints:   = wceq 1243  (class class class)co 5512

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515

This theorem is referenced by:  caov32  5688  oa1suc  6047  nnm1  6097  nnm2  6098  mulidnq  6487  halfnqq  6508  addpinq1  6562  addnqpr1  6660  caucvgprlemm  6766  caucvgprprlemval  6786  caucvgprprlemnbj  6791  caucvgprprlemmu  6793  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  m1p1sr  6845  m1m1sr  6846  0idsr  6852  1idsr  6853  00sr  6854  pn0sr  6856  caucvgsrlemoffres  6884  caucvgsr  6886  mulresr  6914  pitonnlem2  6923  axi2m1  6949  ax1rid  6951  axcnre  6955  add42i  7177  negid  7258  negsub  7259  subneg  7260  negsubdii  7296  apreap  7578  recexaplem2  7633  muleqadd  7649  crap0  7910  2p2e4  8037  3p2e5  8052  3p3e6  8053  4p2e6  8054  4p3e7  8055  4p4e8  8056  5p2e7  8057  5p3e8  8058  5p4e9  8059  5p5e10  8060  6p2e8  8061  6p3e9  8062  6p4e10  8063  7p2e9  8064  7p3e10  8065  8p2e10  8066  3t3e9  8072  8th4div3  8144  halfpm6th  8145  iap0  8148  addltmul  8161  div4p1lem1div2  8177  peano2z  8281  nn0n0n1ge2  8311  nneoor  8340  zeo  8343  numsuc  8379  numltc  8387  numsucc  8393  numma  8398  nummul1c  8403  6p5lem  8416  4t3lem  8438  decbin2  8471  fztp  8940  fzprval  8944  fztpval  8945  fzshftral  8970  fz0tp  8981  fzo01  9072  fzo12sn  9073  fzo0to2pr  9074  fzo0to3tp  9075  fzo0to42pr  9076  intqfrac2  9161  intfracq  9162  sqval  9312  cu2  9351  i3  9354  i4  9355  binom2i  9360  binom3  9366  reim0  9461  cji  9502  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemcalc3  9614  absi  9657  sqr2irrlem  9877