Theorem oveq1i 5898

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

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq1i	|- ( A F C ) = ( B F C )

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq1 5895	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 5	1 |- ( A F C ) = ( B F C )

Syntax hints:   = wceq 1363  (class class class)co 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236  df-ov 5891

This theorem is referenced by:  caov12  6076  map1  6825  halfnqq  7422  prarloclem5  7512  m1m1sr  7773  caucvgsrlemfv  7803  caucvgsr  7814  pitonnlem1  7857  axi2m1  7887  axcnre  7893  axcaucvg  7912  mvrraddi  8187  mvlladdi  8188  negsubdi  8226  mul02  8357  mulneg1  8365  mulreim  8574  recextlem1  8621  recdivap  8688  2p2e4  9059  2times  9060  3p2e5  9073  3p3e6  9074  4p2e6  9075  4p3e7  9076  4p4e8  9077  5p2e7  9078  5p3e8  9079  5p4e9  9080  6p2e8  9081  6p3e9  9082  7p2e9  9083  1mhlfehlf  9150  8th4div3  9151  halfpm6th  9152  nneoor  9368  9p1e10  9399  dfdec10  9400  num0h  9408  numsuc  9410  dec10p  9439  numma  9440  nummac  9441  numma2c  9442  numadd  9443  numaddc  9444  nummul2c  9446  decaddci  9457  decsubi  9459  decmul1  9460  5p5e10  9467  6p4e10  9468  7p3e10  9471  8p2e10  9476  decbin0  9536  decbin2  9537  elfzp1b  10110  elfzm1b  10111  fz01or  10124  fz1ssfz0  10130  fz0to4untppr  10137  qbtwnrelemcalc  10269  fldiv4p1lem1div2  10318  1tonninf  10453  mulexpzap  10573  expaddzap  10577  sq4e2t8  10631  cu2  10632  i3  10635  iexpcyc  10638  binom2i  10642  binom3  10651  3dec  10707  faclbnd  10734  bcm1k  10753  bcp1nk  10755  bcpasc  10759  hashp1i  10803  hashxp  10819  imre  10873  crim  10880  remullem  10893  resqrexlemfp1  11031  resqrexlemover  11032  resqrexlemcalc1  11036  resqrexlemnm  11040  absexpzap  11102  absimle  11106  amgm2  11140  maxabslemlub  11229  fsumconst  11475  modfsummod  11479  binomlem  11504  binom11  11507  arisum  11519  arisum2  11520  georeclim  11534  geo2sum  11535  mertenslemi1  11556  mertenslem2  11557  mertensabs  11558  prodfrecap  11567  fprodm1s  11622  fprodp1s  11623  fprodrec  11650  fprodmodd  11662  efzval  11704  resinval  11736  recosval  11737  efi4p  11738  tan0  11752  efival  11753  cosadd  11758  cos2tsin  11772  ef01bndlem  11777  cos1bnd  11780  cos2bnd  11781  absefib  11791  efieq1re  11792  demoivreALT  11794  eirraplem  11797  3dvdsdec  11883  3dvds2dec  11884  odd2np1  11891  nn0o1gt2  11923  nn0o  11925  flodddiv4  11952  algrp1  12059  3lcm2e6woprm  12099  nn0gcdsq  12213  phiprmpw  12235  prmdiv  12248  prmdiveq  12249  pythagtriplem1  12278  pythagtriplem12  12288  pythagtriplem14  12290  pockthi  12369  infpnlem1  12370  mulg2  13023  subsubg  13088  unitsubm  13362  subsubrng  13429  subsubrg  13460  lsslss  13565  cnmpt1res  14067  rerestcntop  14321  dvfvalap  14421  dvcnp2cntop  14434  dveflem  14458  reeff1oleme  14464  sin0pilem1  14473  sinhalfpilem  14483  cospi  14492  eulerid  14494  cos2pi  14496  ef2kpi  14498  sinhalfpip  14512  sinhalfpim  14513  coshalfpip  14514  coshalfpim  14515  sincosq3sgn  14520  sincosq4sgn  14521  cosq23lt0  14525  tangtx  14530  sincos4thpi  14532  sincos6thpi  14534  cosq34lt1  14542  rplogb1  14637  2logb9irr  14660  sqrt2cxp2logb9e3  14664  2logb9irrap  14666  binom4  14668  lgsdir2lem1  14700  lgsdir2lem2  14701  lgsdir2lem4  14703  lgsdir2lem5  14704  lgsne0  14710  1lgs  14715  lgseisenlem1  14721  lgseisenlem2  14722  m1lgs  14723  2lgsoddprmlem3a  14726  2lgsoddprmlem3b  14727  2lgsoddprmlem3c  14728  2lgsoddprmlem3d  14729  ex-fl  14748  ex-exp  14750  ex-bc  14752  012of  15017  2o01f  15018  qdencn  15047  isomninnlem  15050  iswomninnlem  15069  ismkvnnlem  15072