Theorem oveq1i 5929

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 5926	. 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 1364  (class class class)co 5919

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  caov12  6109  map1  6868  exmidpw2en  6970  halfnqq  7472  prarloclem5  7562  m1m1sr  7823  caucvgsrlemfv  7853  caucvgsr  7864  pitonnlem1  7907  axi2m1  7937  axcnre  7943  axcaucvg  7962  mvrraddi  8238  mvlladdi  8239  negsubdi  8277  mul02  8408  mulneg1  8416  mulreim  8625  recextlem1  8672  recdivap  8739  2p2e4  9111  2times  9112  3p2e5  9126  3p3e6  9127  4p2e6  9128  4p3e7  9129  4p4e8  9130  5p2e7  9131  5p3e8  9132  5p4e9  9133  6p2e8  9134  6p3e9  9135  7p2e9  9136  1mhlfehlf  9203  8th4div3  9204  halfpm6th  9205  nneoor  9422  9p1e10  9453  dfdec10  9454  num0h  9462  numsuc  9464  dec10p  9493  numma  9494  nummac  9495  numma2c  9496  numadd  9497  numaddc  9498  nummul2c  9500  decaddci  9511  decsubi  9513  decmul1  9514  5p5e10  9521  6p4e10  9522  7p3e10  9525  8p2e10  9530  decbin0  9590  decbin2  9591  elfzp1b  10166  elfzm1b  10167  fz01or  10180  fz1ssfz0  10186  fz0to4untppr  10193  qbtwnrelemcalc  10327  fldiv4p1lem1div2  10377  1tonninf  10515  mulexpzap  10653  expaddzap  10657  sq4e2t8  10711  cu2  10712  i3  10715  iexpcyc  10718  binom2i  10722  binom3  10731  3dec  10788  faclbnd  10815  bcm1k  10834  bcp1nk  10836  bcpasc  10840  hashp1i  10884  hashxp  10900  imre  10998  crim  11005  remullem  11018  resqrexlemfp1  11156  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemnm  11165  absexpzap  11227  absimle  11231  amgm2  11265  maxabslemlub  11354  fsumconst  11600  modfsummod  11604  binomlem  11629  binom11  11632  arisum  11644  arisum2  11645  georeclim  11659  geo2sum  11660  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodfrecap  11692  fprodm1s  11747  fprodp1s  11748  fprodrec  11775  fprodmodd  11787  efzval  11829  resinval  11861  recosval  11862  efi4p  11863  tan0  11877  efival  11878  cosadd  11883  cos2tsin  11897  ef01bndlem  11902  cos1bnd  11905  cos2bnd  11906  absefib  11917  efieq1re  11918  demoivreALT  11920  eirraplem  11923  3dvdsdec  12009  3dvds2dec  12010  odd2np1  12017  nn0o1gt2  12049  nn0o  12051  flodddiv4  12078  algrp1  12187  3lcm2e6woprm  12227  nn0gcdsq  12341  phiprmpw  12363  prmdiv  12376  prmdiveq  12377  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem14  12418  pockthi  12499  infpnlem1  12500  4sqlem12  12543  4sqlem13m  12544  4sqlem19  12550  subsubm  13058  mulg2  13204  subsubg  13270  unitsubm  13618  subsubrng  13713  subsubrg  13744  lsslss  13880  expghmap  14106  cnmpt1res  14475  rerestcntop  14737  rerest  14739  dvfvalap  14860  dvcnp2cntop  14878  dveflem  14905  plyun0  14915  dvply1  14943  reeff1oleme  14948  sin0pilem1  14957  sinhalfpilem  14967  cospi  14976  eulerid  14978  cos2pi  14980  ef2kpi  14982  sinhalfpip  14996  sinhalfpim  14997  coshalfpip  14998  coshalfpim  14999  sincosq3sgn  15004  sincosq4sgn  15005  cosq23lt0  15009  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  cosq34lt1  15026  rplogb1  15121  2logb9irr  15144  sqrt2cxp2logb9e3  15148  2logb9irrap  15150  binom4  15152  lgsdir2lem1  15185  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsne0  15195  1lgs  15200  gausslemma2dlem0e  15210  gausslemma2dlem0f  15211  gausslemma2dlem3  15220  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  m1lgs  15242  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem3a  15264  2lgsoddprmlem3b  15265  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  ex-fl  15287  ex-exp  15289  ex-bc  15291  012of  15556  2o01f  15557  qdencn  15587  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612