Theorem oveq1i 5880

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 5877	. 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 1353  (class class class)co 5870

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221  df-ov 5873

This theorem is referenced by:  caov12  6058  map1  6807  halfnqq  7404  prarloclem5  7494  m1m1sr  7755  caucvgsrlemfv  7785  caucvgsr  7796  pitonnlem1  7839  axi2m1  7869  axcnre  7875  axcaucvg  7894  mvrraddi  8168  mvlladdi  8169  negsubdi  8207  mul02  8338  mulneg1  8346  mulreim  8555  recextlem1  8602  recdivap  8669  2p2e4  9040  2times  9041  3p2e5  9054  3p3e6  9055  4p2e6  9056  4p3e7  9057  4p4e8  9058  5p2e7  9059  5p3e8  9060  5p4e9  9061  6p2e8  9062  6p3e9  9063  7p2e9  9064  1mhlfehlf  9131  8th4div3  9132  halfpm6th  9133  nneoor  9349  9p1e10  9380  dfdec10  9381  num0h  9389  numsuc  9391  dec10p  9420  numma  9421  nummac  9422  numma2c  9423  numadd  9424  numaddc  9425  nummul2c  9427  decaddci  9438  decsubi  9440  decmul1  9441  5p5e10  9448  6p4e10  9449  7p3e10  9452  8p2e10  9457  decbin0  9517  decbin2  9518  elfzp1b  10090  elfzm1b  10091  fz01or  10104  fz1ssfz0  10110  fz0to4untppr  10117  qbtwnrelemcalc  10249  fldiv4p1lem1div2  10298  1tonninf  10433  mulexpzap  10553  expaddzap  10557  sq4e2t8  10610  cu2  10611  i3  10614  iexpcyc  10617  binom2i  10621  binom3  10630  3dec  10685  faclbnd  10712  bcm1k  10731  bcp1nk  10733  bcpasc  10737  hashp1i  10781  hashxp  10797  imre  10851  crim  10858  remullem  10871  resqrexlemfp1  11009  resqrexlemover  11010  resqrexlemcalc1  11014  resqrexlemnm  11018  absexpzap  11080  absimle  11084  amgm2  11118  maxabslemlub  11207  fsumconst  11453  modfsummod  11457  binomlem  11482  binom11  11485  arisum  11497  arisum2  11498  georeclim  11512  geo2sum  11513  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  prodfrecap  11545  fprodm1s  11600  fprodp1s  11601  fprodrec  11628  fprodmodd  11640  efzval  11682  resinval  11714  recosval  11715  efi4p  11716  tan0  11730  efival  11731  cosadd  11736  cos2tsin  11750  ef01bndlem  11755  cos1bnd  11758  cos2bnd  11759  absefib  11769  efieq1re  11770  demoivreALT  11772  eirraplem  11775  3dvdsdec  11860  3dvds2dec  11861  odd2np1  11868  nn0o1gt2  11900  nn0o  11902  flodddiv4  11929  algrp1  12036  3lcm2e6woprm  12076  nn0gcdsq  12190  phiprmpw  12212  prmdiv  12225  prmdiveq  12226  pythagtriplem1  12255  pythagtriplem12  12265  pythagtriplem14  12267  pockthi  12346  infpnlem1  12347  mulg2  12920  subsubg  12983  unitsubm  13187  cnmpt1res  13578  rerestcntop  13832  dvfvalap  13932  dvcnp2cntop  13945  dveflem  13969  reeff1oleme  13975  sin0pilem1  13984  sinhalfpilem  13994  cospi  14003  eulerid  14005  cos2pi  14007  ef2kpi  14009  sinhalfpip  14023  sinhalfpim  14024  coshalfpip  14025  coshalfpim  14026  sincosq3sgn  14031  sincosq4sgn  14032  cosq23lt0  14036  tangtx  14041  sincos4thpi  14043  sincos6thpi  14045  cosq34lt1  14053  rplogb1  14148  2logb9irr  14171  sqrt2cxp2logb9e3  14175  2logb9irrap  14177  binom4  14179  lgsdir2lem1  14211  lgsdir2lem2  14212  lgsdir2lem4  14214  lgsdir2lem5  14215  lgsne0  14221  1lgs  14226  ex-fl  14248  ex-exp  14250  ex-bc  14252  012of  14516  2o01f  14517  qdencn  14546  isomninnlem  14549  iswomninnlem  14568  ismkvnnlem  14571