Theorem oveq1i 5884

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 5881	. 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 5874

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 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  caov12  6062  map1  6811  halfnqq  7408  prarloclem5  7498  m1m1sr  7759  caucvgsrlemfv  7789  caucvgsr  7800  pitonnlem1  7843  axi2m1  7873  axcnre  7879  axcaucvg  7898  mvrraddi  8173  mvlladdi  8174  negsubdi  8212  mul02  8343  mulneg1  8351  mulreim  8560  recextlem1  8607  recdivap  8674  2p2e4  9045  2times  9046  3p2e5  9059  3p3e6  9060  4p2e6  9061  4p3e7  9062  4p4e8  9063  5p2e7  9064  5p3e8  9065  5p4e9  9066  6p2e8  9067  6p3e9  9068  7p2e9  9069  1mhlfehlf  9136  8th4div3  9137  halfpm6th  9138  nneoor  9354  9p1e10  9385  dfdec10  9386  num0h  9394  numsuc  9396  dec10p  9425  numma  9426  nummac  9427  numma2c  9428  numadd  9429  numaddc  9430  nummul2c  9432  decaddci  9443  decsubi  9445  decmul1  9446  5p5e10  9453  6p4e10  9454  7p3e10  9457  8p2e10  9462  decbin0  9522  decbin2  9523  elfzp1b  10096  elfzm1b  10097  fz01or  10110  fz1ssfz0  10116  fz0to4untppr  10123  qbtwnrelemcalc  10255  fldiv4p1lem1div2  10304  1tonninf  10439  mulexpzap  10559  expaddzap  10563  sq4e2t8  10617  cu2  10618  i3  10621  iexpcyc  10624  binom2i  10628  binom3  10637  3dec  10693  faclbnd  10720  bcm1k  10739  bcp1nk  10741  bcpasc  10745  hashp1i  10789  hashxp  10805  imre  10859  crim  10866  remullem  10879  resqrexlemfp1  11017  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemnm  11026  absexpzap  11088  absimle  11092  amgm2  11126  maxabslemlub  11215  fsumconst  11461  modfsummod  11465  binomlem  11490  binom11  11493  arisum  11505  arisum2  11506  georeclim  11520  geo2sum  11521  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodfrecap  11553  fprodm1s  11608  fprodp1s  11609  fprodrec  11636  fprodmodd  11648  efzval  11690  resinval  11722  recosval  11723  efi4p  11724  tan0  11738  efival  11739  cosadd  11744  cos2tsin  11758  ef01bndlem  11763  cos1bnd  11766  cos2bnd  11767  absefib  11777  efieq1re  11778  demoivreALT  11780  eirraplem  11783  3dvdsdec  11869  3dvds2dec  11870  odd2np1  11877  nn0o1gt2  11909  nn0o  11911  flodddiv4  11938  algrp1  12045  3lcm2e6woprm  12085  nn0gcdsq  12199  phiprmpw  12221  prmdiv  12234  prmdiveq  12235  pythagtriplem1  12264  pythagtriplem12  12274  pythagtriplem14  12276  pockthi  12355  infpnlem1  12356  mulg2  12991  subsubg  13055  unitsubm  13286  subsubrg  13364  cnmpt1res  13766  rerestcntop  14020  dvfvalap  14120  dvcnp2cntop  14133  dveflem  14157  reeff1oleme  14163  sin0pilem1  14172  sinhalfpilem  14182  cospi  14191  eulerid  14193  cos2pi  14195  ef2kpi  14197  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  sincosq3sgn  14219  sincosq4sgn  14220  cosq23lt0  14224  tangtx  14229  sincos4thpi  14231  sincos6thpi  14233  cosq34lt1  14241  rplogb1  14336  2logb9irr  14359  sqrt2cxp2logb9e3  14363  2logb9irrap  14365  binom4  14367  lgsdir2lem1  14399  lgsdir2lem2  14400  lgsdir2lem4  14402  lgsdir2lem5  14403  lgsne0  14409  1lgs  14414  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2lgsoddprmlem3a  14425  2lgsoddprmlem3b  14426  2lgsoddprmlem3c  14427  2lgsoddprmlem3d  14428  ex-fl  14447  ex-exp  14449  ex-bc  14451  012of  14715  2o01f  14716  qdencn  14745  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770