Theorem oveq1i 5792

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

Syntax hints:   = wceq 1332  (class class class)co 5782

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  caov12  5967  map1  6714  halfnqq  7242  prarloclem5  7332  m1m1sr  7593  caucvgsrlemfv  7623  caucvgsr  7634  pitonnlem1  7677  axi2m1  7707  axcnre  7713  axcaucvg  7732  mvrraddi  8003  mvlladdi  8004  negsubdi  8042  mul02  8173  mulneg1  8181  mulreim  8390  recextlem1  8436  recdivap  8502  2p2e4  8871  2times  8872  3p2e5  8885  3p3e6  8886  4p2e6  8887  4p3e7  8888  4p4e8  8889  5p2e7  8890  5p3e8  8891  5p4e9  8892  6p2e8  8893  6p3e9  8894  7p2e9  8895  1mhlfehlf  8962  8th4div3  8963  halfpm6th  8964  nneoor  9177  9p1e10  9208  dfdec10  9209  num0h  9217  numsuc  9219  dec10p  9248  numma  9249  nummac  9250  numma2c  9251  numadd  9252  numaddc  9253  nummul2c  9255  decaddci  9266  decsubi  9268  decmul1  9269  5p5e10  9276  6p4e10  9277  7p3e10  9280  8p2e10  9285  decbin0  9345  decbin2  9346  elfzp1b  9908  elfzm1b  9909  fz01or  9922  fz1ssfz0  9928  qbtwnrelemcalc  10064  fldiv4p1lem1div2  10109  1tonninf  10244  mulexpzap  10364  expaddzap  10368  sq4e2t8  10421  cu2  10422  i3  10425  iexpcyc  10428  binom2i  10432  binom3  10440  3dec  10492  faclbnd  10519  bcm1k  10538  bcp1nk  10540  bcpasc  10544  hashp1i  10588  hashxp  10604  imre  10655  crim  10662  remullem  10675  resqrexlemfp1  10813  resqrexlemover  10814  resqrexlemcalc1  10818  resqrexlemnm  10822  absexpzap  10884  absimle  10888  amgm2  10922  maxabslemlub  11011  fsumconst  11255  modfsummod  11259  binomlem  11284  binom11  11287  arisum  11299  arisum2  11300  georeclim  11314  geo2sum  11315  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodfrecap  11347  efzval  11426  resinval  11458  recosval  11459  efi4p  11460  tan0  11474  efival  11475  cosadd  11480  cos2tsin  11494  ef01bndlem  11499  cos1bnd  11502  cos2bnd  11503  absefib  11513  efieq1re  11514  demoivreALT  11516  eirraplem  11519  3dvdsdec  11598  3dvds2dec  11599  odd2np1  11606  nn0o1gt2  11638  nn0o  11640  flodddiv4  11667  algrp1  11763  3lcm2e6woprm  11803  nn0gcdsq  11914  phiprmpw  11934  cnmpt1res  12504  rerestcntop  12758  dvfvalap  12858  dvcnp2cntop  12871  dveflem  12895  reeff1oleme  12901  sin0pilem1  12910  sinhalfpilem  12920  cospi  12929  eulerid  12931  cos2pi  12933  ef2kpi  12935  sinhalfpip  12949  sinhalfpim  12950  coshalfpip  12951  coshalfpim  12952  sincosq3sgn  12957  sincosq4sgn  12958  cosq23lt0  12962  tangtx  12967  sincos4thpi  12969  sincos6thpi  12971  cosq34lt1  12979  rplogb1  13073  2logb9irr  13096  sqrt2cxp2logb9e3  13100  2logb9irrap  13102  ex-fl  13108  ex-exp  13110  ex-bc  13112  012of  13363  2o01f  13364  qdencn  13397  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419