Theorem oveq1i 5784

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 5781	. 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 1331  (class class class)co 5774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  caov12  5959  map1  6706  halfnqq  7218  prarloclem5  7308  m1m1sr  7569  caucvgsrlemfv  7599  caucvgsr  7610  pitonnlem1  7653  axi2m1  7683  axcnre  7689  axcaucvg  7708  mvrraddi  7979  mvlladdi  7980  negsubdi  8018  mul02  8149  mulneg1  8157  mulreim  8366  recextlem1  8412  recdivap  8478  2p2e4  8847  2times  8848  3p2e5  8861  3p3e6  8862  4p2e6  8863  4p3e7  8864  4p4e8  8865  5p2e7  8866  5p3e8  8867  5p4e9  8868  6p2e8  8869  6p3e9  8870  7p2e9  8871  1mhlfehlf  8938  8th4div3  8939  halfpm6th  8940  nneoor  9153  9p1e10  9184  dfdec10  9185  num0h  9193  numsuc  9195  dec10p  9224  numma  9225  nummac  9226  numma2c  9227  numadd  9228  numaddc  9229  nummul2c  9231  decaddci  9242  decsubi  9244  decmul1  9245  5p5e10  9252  6p4e10  9253  7p3e10  9256  8p2e10  9261  decbin0  9321  decbin2  9322  elfzp1b  9877  elfzm1b  9878  fz01or  9891  fz1ssfz0  9897  qbtwnrelemcalc  10033  fldiv4p1lem1div2  10078  1tonninf  10213  mulexpzap  10333  expaddzap  10337  sq4e2t8  10390  cu2  10391  i3  10394  iexpcyc  10397  binom2i  10401  binom3  10409  3dec  10461  faclbnd  10487  bcm1k  10506  bcp1nk  10508  bcpasc  10512  hashp1i  10556  hashxp  10572  imre  10623  crim  10630  remullem  10643  resqrexlemfp1  10781  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemnm  10790  absexpzap  10852  absimle  10856  amgm2  10890  maxabslemlub  10979  fsumconst  11223  modfsummod  11227  binomlem  11252  binom11  11255  arisum  11267  arisum2  11268  georeclim  11282  geo2sum  11283  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodfrecap  11315  efzval  11389  resinval  11422  recosval  11423  efi4p  11424  tan0  11438  efival  11439  cosadd  11444  cos2tsin  11458  ef01bndlem  11463  cos1bnd  11466  cos2bnd  11467  absefib  11477  efieq1re  11478  demoivreALT  11480  eirraplem  11483  3dvdsdec  11562  3dvds2dec  11563  odd2np1  11570  nn0o1gt2  11602  nn0o  11604  flodddiv4  11631  algrp1  11727  3lcm2e6woprm  11767  nn0gcdsq  11878  phiprmpw  11898  cnmpt1res  12465  rerestcntop  12719  dvfvalap  12819  dvcnp2cntop  12832  dveflem  12855  sin0pilem1  12862  sinhalfpilem  12872  cospi  12881  eulerid  12883  cos2pi  12885  ef2kpi  12887  sinhalfpip  12901  sinhalfpim  12902  coshalfpip  12903  coshalfpim  12904  sincosq3sgn  12909  sincosq4sgn  12910  cosq23lt0  12914  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  cosq34lt1  12931  ex-fl  12937  ex-exp  12939  ex-bc  12941  qdencn  13222  isomninnlem  13225