Theorem oveq1i 6038

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 6035	. 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 1398  (class class class)co 6028

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  caov12  6221  map1  7030  exmidpw2en  7147  halfnqq  7690  prarloclem5  7780  m1m1sr  8041  caucvgsrlemfv  8071  caucvgsr  8082  pitonnlem1  8125  axi2m1  8155  axcnre  8161  axcaucvg  8180  mvrraddi  8455  mvlladdi  8456  negsubdi  8494  mul02  8625  mulneg1  8633  mulreim  8843  recextlem1  8890  recdivap  8957  2p2e4  9329  2times  9330  3p2e5  9344  3p3e6  9345  4p2e6  9346  4p3e7  9347  4p4e8  9348  5p2e7  9349  5p3e8  9350  5p4e9  9351  6p2e8  9352  6p3e9  9353  7p2e9  9354  1mhlfehlf  9421  8th4div3  9422  halfpm6th  9423  nneoor  9643  9p1e10  9674  dfdec10  9675  num0h  9683  numsuc  9685  dec10p  9714  numma  9715  nummac  9716  numma2c  9717  numadd  9718  numaddc  9719  nummul2c  9721  decaddci  9732  decsubi  9734  decmul1  9735  5p5e10  9742  6p4e10  9743  7p3e10  9746  8p2e10  9751  decbin0  9811  decbin2  9812  elfzp1b  10394  elfzm1b  10395  fz01or  10408  fz1ssfz0  10414  fz0to4untppr  10421  qbtwnrelemcalc  10578  fldiv4p1lem1div2  10628  1tonninf  10766  mulexpzap  10904  expaddzap  10908  sq4e2t8  10962  cu2  10963  i3  10966  iexpcyc  10969  binom2i  10973  binom3  10982  3dec  11039  faclbnd  11066  bcm1k  11085  bcp1nk  11087  bcpasc  11091  hashp1i  11137  hashxp  11153  ccatlid  11249  pfxccatin12lem2c  11377  imre  11491  crim  11498  remullem  11511  resqrexlemfp1  11649  resqrexlemover  11650  resqrexlemcalc1  11654  resqrexlemnm  11658  absexpzap  11720  absimle  11724  amgm2  11758  maxabslemlub  11847  fsumconst  12095  modfsummod  12099  binomlem  12124  binom11  12127  arisum  12139  arisum2  12140  georeclim  12154  geo2sum  12155  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodfrecap  12187  fprodm1s  12242  fprodp1s  12243  fprodrec  12270  fprodmodd  12282  efzval  12324  resinval  12356  recosval  12357  efi4p  12358  tan0  12372  efival  12373  cosadd  12378  cos2tsin  12392  ef01bndlem  12397  cos1bnd  12400  cos2bnd  12401  absefib  12412  efieq1re  12413  demoivreALT  12415  eirraplem  12418  3dvds  12505  3dvdsdec  12506  3dvds2dec  12507  odd2np1  12514  nn0o1gt2  12546  nn0o  12548  5ndvds3  12575  5ndvds6  12576  flodddiv4  12577  m1bits  12601  algrp1  12698  3lcm2e6woprm  12738  nn0gcdsq  12852  phiprmpw  12874  prmdiv  12887  prmdiveq  12888  pythagtriplem1  12918  pythagtriplem12  12928  pythagtriplem14  12930  pockthi  13011  infpnlem1  13012  4sqlem12  13055  4sqlem13m  13056  4sqlem19  13062  dec5dvds  13065  dec5nprm  13067  dec2nprm  13068  modxai  13069  modxp1i  13071  modsubi  13072  gcdmodi  13074  decsplit0b  13079  decsplit1  13081  decsplit  13082  karatsuba  13083  2exp7  13087  2exp8  13088  3exp3  13091  pwsbas  13455  subsubm  13646  mulg2  13798  subsubg  13864  unitsubm  14214  subsubrng  14309  subsubrg  14340  lsslss  14477  expghmap  14703  cnmpt1res  15107  rerestcntop  15369  rerest  15371  dvfvalap  15492  dvcnp2cntop  15510  dveflem  15537  plyun0  15547  dvply1  15576  reeff1oleme  15583  sin0pilem1  15592  sinhalfpilem  15602  cospi  15611  eulerid  15613  cos2pi  15615  ef2kpi  15617  sinhalfpip  15631  sinhalfpim  15632  coshalfpip  15633  coshalfpim  15634  sincosq3sgn  15639  sincosq4sgn  15640  cosq23lt0  15644  tangtx  15649  sincos4thpi  15651  sincos6thpi  15653  cosq34lt1  15661  rplogb1  15759  2logb9irr  15782  sqrt2cxp2logb9e3  15786  2logb9irrap  15788  binom4  15790  lgsdir2lem1  15847  lgsdir2lem2  15848  lgsdir2lem4  15850  lgsdir2lem5  15851  lgsne0  15857  1lgs  15862  gausslemma2dlem0e  15872  gausslemma2dlem0f  15873  gausslemma2dlem3  15882  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  lgsquad2lem2  15901  m1lgs  15904  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgsoddprmlem3a  15926  2lgsoddprmlem3b  15927  2lgsoddprmlem3c  15928  2lgsoddprmlem3d  15929  ex-fl  16439  ex-exp  16441  ex-bc  16443  depindlem1  16447  012of  16713  2o01f  16714  qdencn  16755  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785