Theorem oveq1i 5828

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

Syntax hints:   = wceq 1335  (class class class)co 5818

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-iota 5132  df-fv 5175  df-ov 5821

This theorem is referenced by:  caov12  6003  map1  6750  halfnqq  7313  prarloclem5  7403  m1m1sr  7664  caucvgsrlemfv  7694  caucvgsr  7705  pitonnlem1  7748  axi2m1  7778  axcnre  7784  axcaucvg  7803  mvrraddi  8075  mvlladdi  8076  negsubdi  8114  mul02  8245  mulneg1  8253  mulreim  8462  recextlem1  8508  recdivap  8574  2p2e4  8943  2times  8944  3p2e5  8957  3p3e6  8958  4p2e6  8959  4p3e7  8960  4p4e8  8961  5p2e7  8962  5p3e8  8963  5p4e9  8964  6p2e8  8965  6p3e9  8966  7p2e9  8967  1mhlfehlf  9034  8th4div3  9035  halfpm6th  9036  nneoor  9249  9p1e10  9280  dfdec10  9281  num0h  9289  numsuc  9291  dec10p  9320  numma  9321  nummac  9322  numma2c  9323  numadd  9324  numaddc  9325  nummul2c  9327  decaddci  9338  decsubi  9340  decmul1  9341  5p5e10  9348  6p4e10  9349  7p3e10  9352  8p2e10  9357  decbin0  9417  decbin2  9418  elfzp1b  9981  elfzm1b  9982  fz01or  9995  fz1ssfz0  10001  qbtwnrelemcalc  10137  fldiv4p1lem1div2  10186  1tonninf  10321  mulexpzap  10441  expaddzap  10445  sq4e2t8  10498  cu2  10499  i3  10502  iexpcyc  10505  binom2i  10509  binom3  10517  3dec  10570  faclbnd  10597  bcm1k  10616  bcp1nk  10618  bcpasc  10622  hashp1i  10666  hashxp  10682  imre  10733  crim  10740  remullem  10753  resqrexlemfp1  10891  resqrexlemover  10892  resqrexlemcalc1  10896  resqrexlemnm  10900  absexpzap  10962  absimle  10966  amgm2  11000  maxabslemlub  11089  fsumconst  11333  modfsummod  11337  binomlem  11362  binom11  11365  arisum  11377  arisum2  11378  georeclim  11392  geo2sum  11393  mertenslemi1  11414  mertenslem2  11415  mertensabs  11416  prodfrecap  11425  fprodm1s  11480  fprodp1s  11481  fprodrec  11508  fprodmodd  11520  efzval  11562  resinval  11594  recosval  11595  efi4p  11596  tan0  11610  efival  11611  cosadd  11616  cos2tsin  11630  ef01bndlem  11635  cos1bnd  11638  cos2bnd  11639  absefib  11649  efieq1re  11650  demoivreALT  11652  eirraplem  11655  3dvdsdec  11737  3dvds2dec  11738  odd2np1  11745  nn0o1gt2  11777  nn0o  11779  flodddiv4  11806  algrp1  11903  3lcm2e6woprm  11943  nn0gcdsq  12054  phiprmpw  12074  prmdiv  12087  prmdiveq  12088  cnmpt1res  12656  rerestcntop  12910  dvfvalap  13010  dvcnp2cntop  13023  dveflem  13047  reeff1oleme  13053  sin0pilem1  13062  sinhalfpilem  13072  cospi  13081  eulerid  13083  cos2pi  13085  ef2kpi  13087  sinhalfpip  13101  sinhalfpim  13102  coshalfpip  13103  coshalfpim  13104  sincosq3sgn  13109  sincosq4sgn  13110  cosq23lt0  13114  tangtx  13119  sincos4thpi  13121  sincos6thpi  13123  cosq34lt1  13131  rplogb1  13225  2logb9irr  13248  sqrt2cxp2logb9e3  13252  2logb9irrap  13254  binom4  13256  ex-fl  13261  ex-exp  13263  ex-bc  13265  012of  13528  2o01f  13529  qdencn  13561  isomninnlem  13564  iswomninnlem  13583  ismkvnnlem  13586