Theorem oveq1i 5777

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

Syntax hints:   = wceq 1331  (class class class)co 5767

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770

This theorem is referenced by:  caov12  5952  map1  6699  halfnqq  7211  prarloclem5  7301  m1m1sr  7562  caucvgsrlemfv  7592  caucvgsr  7603  pitonnlem1  7646  axi2m1  7676  axcnre  7682  axcaucvg  7701  mvrraddi  7972  mvlladdi  7973  negsubdi  8011  mul02  8142  mulneg1  8150  mulreim  8359  recextlem1  8405  recdivap  8471  2p2e4  8840  2times  8841  3p2e5  8854  3p3e6  8855  4p2e6  8856  4p3e7  8857  4p4e8  8858  5p2e7  8859  5p3e8  8860  5p4e9  8861  6p2e8  8862  6p3e9  8863  7p2e9  8864  1mhlfehlf  8931  8th4div3  8932  halfpm6th  8933  nneoor  9146  9p1e10  9177  dfdec10  9178  num0h  9186  numsuc  9188  dec10p  9217  numma  9218  nummac  9219  numma2c  9220  numadd  9221  numaddc  9222  nummul2c  9224  decaddci  9235  decsubi  9237  decmul1  9238  5p5e10  9245  6p4e10  9246  7p3e10  9249  8p2e10  9254  decbin0  9314  decbin2  9315  elfzp1b  9870  elfzm1b  9871  fz01or  9884  fz1ssfz0  9890  qbtwnrelemcalc  10026  fldiv4p1lem1div2  10071  1tonninf  10206  mulexpzap  10326  expaddzap  10330  sq4e2t8  10383  cu2  10384  i3  10387  iexpcyc  10390  binom2i  10394  binom3  10402  3dec  10454  faclbnd  10480  bcm1k  10499  bcp1nk  10501  bcpasc  10505  hashp1i  10549  hashxp  10565  imre  10616  crim  10623  remullem  10636  resqrexlemfp1  10774  resqrexlemover  10775  resqrexlemcalc1  10779  resqrexlemnm  10783  absexpzap  10845  absimle  10849  amgm2  10883  maxabslemlub  10972  fsumconst  11216  modfsummod  11220  binomlem  11245  binom11  11248  arisum  11260  arisum2  11261  georeclim  11275  geo2sum  11276  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodfrecap  11308  efzval  11378  resinval  11411  recosval  11412  efi4p  11413  tan0  11427  efival  11428  cosadd  11433  cos2tsin  11447  ef01bndlem  11452  cos1bnd  11455  cos2bnd  11456  absefib  11466  efieq1re  11467  demoivreALT  11469  eirraplem  11472  3dvdsdec  11551  3dvds2dec  11552  odd2np1  11559  nn0o1gt2  11591  nn0o  11593  flodddiv4  11620  algrp1  11716  3lcm2e6woprm  11756  nn0gcdsq  11867  phiprmpw  11887  cnmpt1res  12454  rerestcntop  12708  dvfvalap  12808  dvcnp2cntop  12821  dveflem  12844  sin0pilem1  12851  sinhalfpilem  12861  cospi  12870  eulerid  12872  cos2pi  12874  ef2kpi  12876  sinhalfpip  12890  sinhalfpim  12891  coshalfpip  12892  coshalfpim  12893  sincosq3sgn  12898  sincosq4sgn  12899  cosq23lt0  12903  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  cosq34lt1  12920  ex-fl  12926  ex-exp  12928  ex-bc  12930  qdencn  13211  isomninnlem  13214