Theorem oveq1i 6085

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 6082	. 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 1402  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  caov12  6268  map1  7091  exmidpw2en  7209  halfnqq  7767  prarloclem5  7857  m1m1sr  8118  caucvgsrlemfv  8148  caucvgsr  8159  pitonnlem1  8202  axi2m1  8232  axcnre  8238  axcaucvg  8257  mvrraddi  8533  mvlladdi  8534  negsubdi  8572  mul02  8704  mulneg1  8712  mulreim  8922  recextlem1  8969  recdivap  9038  2p2e4  9410  2times  9411  3p2e5  9425  3p3e6  9426  4p2e6  9427  4p3e7  9428  4p4e8  9429  5p2e7  9430  5p3e8  9431  5p4e9  9432  6p2e8  9433  6p3e9  9434  7p2e9  9435  1mhlfehlf  9502  8th4div3  9503  halfpm6th  9504  nneoor  9727  9p1e10  9758  dfdec10  9759  num0h  9767  numsuc  9769  dec10p  9798  numma  9799  nummac  9800  numma2c  9801  numadd  9802  numaddc  9803  nummul2c  9805  decaddci  9816  decsubi  9818  decmul1  9819  5p5e10  9826  6p4e10  9827  7p3e10  9830  8p2e10  9835  decbin0  9895  decbin2  9896  elfzp1b  10482  elfzm1b  10483  fz01or  10496  fz1ssfz0  10502  fz0to4untppr  10509  qbtwnrelemcalc  10668  fldiv4p1lem1div2  10718  1tonninf  10856  mulexpzap  10994  expaddzap  10998  sq4e2t8  11052  cu2  11053  i3  11056  iexpcyc  11059  binom2i  11063  binom3  11072  3dec  11130  faclbnd  11157  bcm1k  11176  bcp1nk  11178  bcpasc  11182  hashp1i  11229  hashxp  11245  hashpwfi  11247  hashfibc  11261  ccatlid  11352  pfxccatin12lem2c  11480  imre  11594  crim  11601  remullem  11614  sq01  11638  resqrexlemfp1  11753  resqrexlemover  11754  resqrexlemcalc1  11758  resqrexlemnm  11762  absexpzap  11824  absimle  11828  amgm2  11862  maxabslemlub  11951  fsumconst  12199  modfsummod  12203  binomlem  12228  binom11  12231  arisum  12243  arisum2  12244  georeclim  12258  geo2sum  12259  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodfrecap  12291  fprodm1s  12346  fprodp1s  12347  fprodrec  12374  fprodmodd  12386  efzval  12428  resinval  12460  recosval  12461  efi4p  12462  tan0  12476  efival  12477  cosadd  12482  cos2tsin  12496  ef01bndlem  12501  cos1bnd  12504  cos2bnd  12505  absefib  12516  efieq1re  12517  demoivreALT  12519  eirraplem  12522  3dvds  12609  3dvdsdec  12610  3dvds2dec  12611  odd2np1  12618  nn0o1gt2  12650  nn0o  12652  5ndvds3  12679  5ndvds6  12680  flodddiv4  12681  m1bits  12705  algrp1  12802  3lcm2e6woprm  12842  nn0gcdsq  12956  phiprmpw  12978  prmdiv  12991  prmdiveq  12992  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem14  13034  pockthi  13115  infpnlem1  13116  4sqlem12  13159  4sqlem13m  13160  4sqlem19  13166  dec5dvds  13169  dec5nprm  13171  dec2nprm  13172  modxai  13173  modxp1i  13175  modsubi  13176  gcdmodi  13178  decsplit0b  13183  decsplit1  13185  decsplit  13186  karatsuba  13187  2exp7  13191  2exp8  13192  3exp3  13195  ballotfilem1  13198  ballotfilem2  13206  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemfrceq  13250  ballotfilemth  13259  subsubm  13767  mulg2  13911  subsubg  13977  gsumconstcmn  14143  pwsbas  14182  unitsubm  14399  subsubrng  14495  subsubrg  14526  lsslss  14690  expghmap  14914  cnmpt1res  15320  rerestcntop  15582  rerest  15584  dvfvalap  15705  dvcnp2cntop  15723  dveflem  15750  plyun0  15760  dvply1  15789  reeff1oleme  15796  sin0pilem1  15805  sinhalfpilem  15815  cospi  15824  eulerid  15826  cos2pi  15828  ef2kpi  15830  sinhalfpip  15844  sinhalfpim  15845  coshalfpip  15846  coshalfpim  15847  sincosq3sgn  15852  sincosq4sgn  15853  cosq23lt0  15857  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  cosq34lt1  15874  logfac  15918  rplogb1  15973  2logb9irr  15996  sqrt2cxp2logb9e3  16000  2logb9irrap  16002  binom4  16004  lgsdir2lem1  16061  lgsdir2lem2  16062  lgsdir2lem4  16064  lgsdir2lem5  16065  lgsne0  16071  1lgs  16076  gausslemma2dlem0e  16086  gausslemma2dlem0f  16087  gausslemma2dlem3  16096  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  lgsquad2lem2  16115  m1lgs  16118  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgsoddprmlem3a  16140  2lgsoddprmlem3b  16141  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143  ex-fl  16653  ex-exp  16655  ex-bc  16657  depindlem1  16661  012of  16937  2o01f  16938  qdencn  16977  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007