Theorem oveq1i 5933

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 5930	. 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 5923

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5926

This theorem is referenced by:  caov12  6114  map1  6873  exmidpw2en  6975  halfnqq  7480  prarloclem5  7570  m1m1sr  7831  caucvgsrlemfv  7861  caucvgsr  7872  pitonnlem1  7915  axi2m1  7945  axcnre  7951  axcaucvg  7970  mvrraddi  8246  mvlladdi  8247  negsubdi  8285  mul02  8416  mulneg1  8424  mulreim  8634  recextlem1  8681  recdivap  8748  2p2e4  9120  2times  9121  3p2e5  9135  3p3e6  9136  4p2e6  9137  4p3e7  9138  4p4e8  9139  5p2e7  9140  5p3e8  9141  5p4e9  9142  6p2e8  9143  6p3e9  9144  7p2e9  9145  1mhlfehlf  9212  8th4div3  9213  halfpm6th  9214  nneoor  9431  9p1e10  9462  dfdec10  9463  num0h  9471  numsuc  9473  dec10p  9502  numma  9503  nummac  9504  numma2c  9505  numadd  9506  numaddc  9507  nummul2c  9509  decaddci  9520  decsubi  9522  decmul1  9523  5p5e10  9530  6p4e10  9531  7p3e10  9534  8p2e10  9539  decbin0  9599  decbin2  9600  elfzp1b  10175  elfzm1b  10176  fz01or  10189  fz1ssfz0  10195  fz0to4untppr  10202  qbtwnrelemcalc  10348  fldiv4p1lem1div2  10398  1tonninf  10536  mulexpzap  10674  expaddzap  10678  sq4e2t8  10732  cu2  10733  i3  10736  iexpcyc  10739  binom2i  10743  binom3  10752  3dec  10809  faclbnd  10836  bcm1k  10855  bcp1nk  10857  bcpasc  10861  hashp1i  10905  hashxp  10921  imre  11019  crim  11026  remullem  11039  resqrexlemfp1  11177  resqrexlemover  11178  resqrexlemcalc1  11182  resqrexlemnm  11186  absexpzap  11248  absimle  11252  amgm2  11286  maxabslemlub  11375  fsumconst  11622  modfsummod  11626  binomlem  11651  binom11  11654  arisum  11666  arisum2  11667  georeclim  11681  geo2sum  11682  mertenslemi1  11703  mertenslem2  11704  mertensabs  11705  prodfrecap  11714  fprodm1s  11769  fprodp1s  11770  fprodrec  11797  fprodmodd  11809  efzval  11851  resinval  11883  recosval  11884  efi4p  11885  tan0  11899  efival  11900  cosadd  11905  cos2tsin  11919  ef01bndlem  11924  cos1bnd  11927  cos2bnd  11928  absefib  11939  efieq1re  11940  demoivreALT  11942  eirraplem  11945  3dvds  12032  3dvdsdec  12033  3dvds2dec  12034  odd2np1  12041  nn0o1gt2  12073  nn0o  12075  5ndvds3  12102  5ndvds6  12103  flodddiv4  12104  m1bits  12128  algrp1  12225  3lcm2e6woprm  12265  nn0gcdsq  12379  phiprmpw  12401  prmdiv  12414  prmdiveq  12415  pythagtriplem1  12445  pythagtriplem12  12455  pythagtriplem14  12457  pockthi  12538  infpnlem1  12539  4sqlem12  12582  4sqlem13m  12583  4sqlem19  12589  dec5dvds  12592  dec5nprm  12594  dec2nprm  12595  modxai  12596  modxp1i  12598  modsubi  12599  gcdmodi  12601  decsplit0b  12606  decsplit1  12608  decsplit  12609  karatsuba  12610  2exp7  12614  2exp8  12615  3exp3  12618  subsubm  13141  mulg2  13287  subsubg  13353  unitsubm  13701  subsubrng  13796  subsubrg  13827  lsslss  13963  expghmap  14189  cnmpt1res  14558  rerestcntop  14820  rerest  14822  dvfvalap  14943  dvcnp2cntop  14961  dveflem  14988  plyun0  14998  dvply1  15027  reeff1oleme  15034  sin0pilem1  15043  sinhalfpilem  15053  cospi  15062  eulerid  15064  cos2pi  15066  ef2kpi  15068  sinhalfpip  15082  sinhalfpim  15083  coshalfpip  15084  coshalfpim  15085  sincosq3sgn  15090  sincosq4sgn  15091  cosq23lt0  15095  tangtx  15100  sincos4thpi  15102  sincos6thpi  15104  cosq34lt1  15112  rplogb1  15210  2logb9irr  15233  sqrt2cxp2logb9e3  15237  2logb9irrap  15239  binom4  15241  lgsdir2lem1  15295  lgsdir2lem2  15296  lgsdir2lem4  15298  lgsdir2lem5  15299  lgsne0  15305  1lgs  15310  gausslemma2dlem0e  15320  gausslemma2dlem0f  15321  gausslemma2dlem3  15330  gausslemma2d  15336  lgseisenlem1  15337  lgseisenlem2  15338  lgseisenlem3  15339  lgseisenlem4  15340  lgseisen  15341  lgsquadlem1  15344  lgsquadlem2  15345  lgsquad2lem1  15348  lgsquad2lem2  15349  m1lgs  15352  2lgslem3a  15360  2lgslem3b  15361  2lgslem3c  15362  2lgslem3d  15363  2lgsoddprmlem3a  15374  2lgsoddprmlem3b  15375  2lgsoddprmlem3c  15376  2lgsoddprmlem3d  15377  ex-fl  15397  ex-exp  15399  ex-bc  15401  012of  15666  2o01f  15667  qdencn  15698  isomninnlem  15701  iswomninnlem  15720  ismkvnnlem  15723