Theorem oveq1i 6011

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 6008	. 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 1395  (class class class)co 6001

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  caov12  6194  map1  6965  exmidpw2en  7074  halfnqq  7597  prarloclem5  7687  m1m1sr  7948  caucvgsrlemfv  7978  caucvgsr  7989  pitonnlem1  8032  axi2m1  8062  axcnre  8068  axcaucvg  8087  mvrraddi  8363  mvlladdi  8364  negsubdi  8402  mul02  8533  mulneg1  8541  mulreim  8751  recextlem1  8798  recdivap  8865  2p2e4  9237  2times  9238  3p2e5  9252  3p3e6  9253  4p2e6  9254  4p3e7  9255  4p4e8  9256  5p2e7  9257  5p3e8  9258  5p4e9  9259  6p2e8  9260  6p3e9  9261  7p2e9  9262  1mhlfehlf  9329  8th4div3  9330  halfpm6th  9331  nneoor  9549  9p1e10  9580  dfdec10  9581  num0h  9589  numsuc  9591  dec10p  9620  numma  9621  nummac  9622  numma2c  9623  numadd  9624  numaddc  9625  nummul2c  9627  decaddci  9638  decsubi  9640  decmul1  9641  5p5e10  9648  6p4e10  9649  7p3e10  9652  8p2e10  9657  decbin0  9717  decbin2  9718  elfzp1b  10293  elfzm1b  10294  fz01or  10307  fz1ssfz0  10313  fz0to4untppr  10320  qbtwnrelemcalc  10475  fldiv4p1lem1div2  10525  1tonninf  10663  mulexpzap  10801  expaddzap  10805  sq4e2t8  10859  cu2  10860  i3  10863  iexpcyc  10866  binom2i  10870  binom3  10879  3dec  10936  faclbnd  10963  bcm1k  10982  bcp1nk  10984  bcpasc  10988  hashp1i  11032  hashxp  11048  ccatlid  11141  pfxccatin12lem2c  11262  imre  11362  crim  11369  remullem  11382  resqrexlemfp1  11520  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemnm  11529  absexpzap  11591  absimle  11595  amgm2  11629  maxabslemlub  11718  fsumconst  11965  modfsummod  11969  binomlem  11994  binom11  11997  arisum  12009  arisum2  12010  georeclim  12024  geo2sum  12025  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodfrecap  12057  fprodm1s  12112  fprodp1s  12113  fprodrec  12140  fprodmodd  12152  efzval  12194  resinval  12226  recosval  12227  efi4p  12228  tan0  12242  efival  12243  cosadd  12248  cos2tsin  12262  ef01bndlem  12267  cos1bnd  12270  cos2bnd  12271  absefib  12282  efieq1re  12283  demoivreALT  12285  eirraplem  12288  3dvds  12375  3dvdsdec  12376  3dvds2dec  12377  odd2np1  12384  nn0o1gt2  12416  nn0o  12418  5ndvds3  12445  5ndvds6  12446  flodddiv4  12447  m1bits  12471  algrp1  12568  3lcm2e6woprm  12608  nn0gcdsq  12722  phiprmpw  12744  prmdiv  12757  prmdiveq  12758  pythagtriplem1  12788  pythagtriplem12  12798  pythagtriplem14  12800  pockthi  12881  infpnlem1  12882  4sqlem12  12925  4sqlem13m  12926  4sqlem19  12932  dec5dvds  12935  dec5nprm  12937  dec2nprm  12938  modxai  12939  modxp1i  12941  modsubi  12942  gcdmodi  12944  decsplit0b  12949  decsplit1  12951  decsplit  12952  karatsuba  12953  2exp7  12957  2exp8  12958  3exp3  12961  pwsbas  13325  subsubm  13516  mulg2  13668  subsubg  13734  unitsubm  14083  subsubrng  14178  subsubrg  14209  lsslss  14345  expghmap  14571  cnmpt1res  14970  rerestcntop  15232  rerest  15234  dvfvalap  15355  dvcnp2cntop  15373  dveflem  15400  plyun0  15410  dvply1  15439  reeff1oleme  15446  sin0pilem1  15455  sinhalfpilem  15465  cospi  15474  eulerid  15476  cos2pi  15478  ef2kpi  15480  sinhalfpip  15494  sinhalfpim  15495  coshalfpip  15496  coshalfpim  15497  sincosq3sgn  15502  sincosq4sgn  15503  cosq23lt0  15507  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  cosq34lt1  15524  rplogb1  15622  2logb9irr  15645  sqrt2cxp2logb9e3  15649  2logb9irrap  15651  binom4  15653  lgsdir2lem1  15707  lgsdir2lem2  15708  lgsdir2lem4  15710  lgsdir2lem5  15711  lgsne0  15717  1lgs  15722  gausslemma2dlem0e  15732  gausslemma2dlem0f  15733  gausslemma2dlem3  15742  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  lgsquad2lem2  15761  m1lgs  15764  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgsoddprmlem3a  15786  2lgsoddprmlem3b  15787  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  ex-fl  16089  ex-exp  16091  ex-bc  16093  012of  16357  2o01f  16358  qdencn  16395  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420