Theorem oveq1i 5863

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

Syntax hints:   = wceq 1348  (class class class)co 5853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  caov12  6041  map1  6790  halfnqq  7372  prarloclem5  7462  m1m1sr  7723  caucvgsrlemfv  7753  caucvgsr  7764  pitonnlem1  7807  axi2m1  7837  axcnre  7843  axcaucvg  7862  mvrraddi  8136  mvlladdi  8137  negsubdi  8175  mul02  8306  mulneg1  8314  mulreim  8523  recextlem1  8569  recdivap  8635  2p2e4  9005  2times  9006  3p2e5  9019  3p3e6  9020  4p2e6  9021  4p3e7  9022  4p4e8  9023  5p2e7  9024  5p3e8  9025  5p4e9  9026  6p2e8  9027  6p3e9  9028  7p2e9  9029  1mhlfehlf  9096  8th4div3  9097  halfpm6th  9098  nneoor  9314  9p1e10  9345  dfdec10  9346  num0h  9354  numsuc  9356  dec10p  9385  numma  9386  nummac  9387  numma2c  9388  numadd  9389  numaddc  9390  nummul2c  9392  decaddci  9403  decsubi  9405  decmul1  9406  5p5e10  9413  6p4e10  9414  7p3e10  9417  8p2e10  9422  decbin0  9482  decbin2  9483  elfzp1b  10053  elfzm1b  10054  fz01or  10067  fz1ssfz0  10073  fz0to4untppr  10080  qbtwnrelemcalc  10212  fldiv4p1lem1div2  10261  1tonninf  10396  mulexpzap  10516  expaddzap  10520  sq4e2t8  10573  cu2  10574  i3  10577  iexpcyc  10580  binom2i  10584  binom3  10593  3dec  10648  faclbnd  10675  bcm1k  10694  bcp1nk  10696  bcpasc  10700  hashp1i  10745  hashxp  10761  imre  10815  crim  10822  remullem  10835  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemnm  10982  absexpzap  11044  absimle  11048  amgm2  11082  maxabslemlub  11171  fsumconst  11417  modfsummod  11421  binomlem  11446  binom11  11449  arisum  11461  arisum2  11462  georeclim  11476  geo2sum  11477  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodfrecap  11509  fprodm1s  11564  fprodp1s  11565  fprodrec  11592  fprodmodd  11604  efzval  11646  resinval  11678  recosval  11679  efi4p  11680  tan0  11694  efival  11695  cosadd  11700  cos2tsin  11714  ef01bndlem  11719  cos1bnd  11722  cos2bnd  11723  absefib  11733  efieq1re  11734  demoivreALT  11736  eirraplem  11739  3dvdsdec  11824  3dvds2dec  11825  odd2np1  11832  nn0o1gt2  11864  nn0o  11866  flodddiv4  11893  algrp1  12000  3lcm2e6woprm  12040  nn0gcdsq  12154  phiprmpw  12176  prmdiv  12189  prmdiveq  12190  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem14  12231  pockthi  12310  infpnlem1  12311  cnmpt1res  13090  rerestcntop  13344  dvfvalap  13444  dvcnp2cntop  13457  dveflem  13481  reeff1oleme  13487  sin0pilem1  13496  sinhalfpilem  13506  cospi  13515  eulerid  13517  cos2pi  13519  ef2kpi  13521  sinhalfpip  13535  sinhalfpim  13536  coshalfpip  13537  coshalfpim  13538  sincosq3sgn  13543  sincosq4sgn  13544  cosq23lt0  13548  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  cosq34lt1  13565  rplogb1  13660  2logb9irr  13683  sqrt2cxp2logb9e3  13687  2logb9irrap  13689  binom4  13691  lgsdir2lem1  13723  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsne0  13733  1lgs  13738  ex-fl  13760  ex-exp  13762  ex-bc  13764  012of  14028  2o01f  14029  qdencn  14059  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084