Theorem oveq1i 5522

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq1 5519	. 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:  caov12  5689  halfnqq  6508  prarloclem5  6598  m1m1sr  6846  caucvgsrlemfv  6875  caucvgsr  6886  pitonnlem1  6921  axi2m1  6949  axcnre  6955  axcaucvg  6974  mvrraddi  7228  mvlladdi  7229  negsubdi  7267  mul02  7384  mulneg1  7392  mulreim  7595  recextlem1  7632  recdivap  7694  2p2e4  8037  2times  8038  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  1mhlfehlf  8143  8th4div3  8144  halfpm6th  8145  nneoor  8340  num0h  8377  numsuc  8379  dec10p  8396  numma  8398  nummac  8399  numma2c  8400  numadd  8401  numaddc  8402  nummul2c  8404  decaddci  8412  decbin0  8470  decbin2  8471  elfzp1b  8959  elfzm1b  8960  qbtwnrelemcalc  9110  fldiv4p1lem1div2  9147  mulexpzap  9295  expaddzap  9299  cu2  9351  i3  9354  binom2i  9360  binom3  9366  imre  9451  crim  9458  remullem  9471  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemnm  9616  absexpzap  9676  absimle  9680  amgm2  9714  ex-fl  9895  qdencn  10124