Theorem oveq1i 6017

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 6014	. 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 6007

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 6010

This theorem is referenced by:  caov12  6200  map1  6973  exmidpw2en  7085  halfnqq  7608  prarloclem5  7698  m1m1sr  7959  caucvgsrlemfv  7989  caucvgsr  8000  pitonnlem1  8043  axi2m1  8073  axcnre  8079  axcaucvg  8098  mvrraddi  8374  mvlladdi  8375  negsubdi  8413  mul02  8544  mulneg1  8552  mulreim  8762  recextlem1  8809  recdivap  8876  2p2e4  9248  2times  9249  3p2e5  9263  3p3e6  9264  4p2e6  9265  4p3e7  9266  4p4e8  9267  5p2e7  9268  5p3e8  9269  5p4e9  9270  6p2e8  9271  6p3e9  9272  7p2e9  9273  1mhlfehlf  9340  8th4div3  9341  halfpm6th  9342  nneoor  9560  9p1e10  9591  dfdec10  9592  num0h  9600  numsuc  9602  dec10p  9631  numma  9632  nummac  9633  numma2c  9634  numadd  9635  numaddc  9636  nummul2c  9638  decaddci  9649  decsubi  9651  decmul1  9652  5p5e10  9659  6p4e10  9660  7p3e10  9663  8p2e10  9668  decbin0  9728  decbin2  9729  elfzp1b  10305  elfzm1b  10306  fz01or  10319  fz1ssfz0  10325  fz0to4untppr  10332  qbtwnrelemcalc  10487  fldiv4p1lem1div2  10537  1tonninf  10675  mulexpzap  10813  expaddzap  10817  sq4e2t8  10871  cu2  10872  i3  10875  iexpcyc  10878  binom2i  10882  binom3  10891  3dec  10948  faclbnd  10975  bcm1k  10994  bcp1nk  10996  bcpasc  11000  hashp1i  11045  hashxp  11061  ccatlid  11154  pfxccatin12lem2c  11278  imre  11378  crim  11385  remullem  11398  resqrexlemfp1  11536  resqrexlemover  11537  resqrexlemcalc1  11541  resqrexlemnm  11545  absexpzap  11607  absimle  11611  amgm2  11645  maxabslemlub  11734  fsumconst  11981  modfsummod  11985  binomlem  12010  binom11  12013  arisum  12025  arisum2  12026  georeclim  12040  geo2sum  12041  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodfrecap  12073  fprodm1s  12128  fprodp1s  12129  fprodrec  12156  fprodmodd  12168  efzval  12210  resinval  12242  recosval  12243  efi4p  12244  tan0  12258  efival  12259  cosadd  12264  cos2tsin  12278  ef01bndlem  12283  cos1bnd  12286  cos2bnd  12287  absefib  12298  efieq1re  12299  demoivreALT  12301  eirraplem  12304  3dvds  12391  3dvdsdec  12392  3dvds2dec  12393  odd2np1  12400  nn0o1gt2  12432  nn0o  12434  5ndvds3  12461  5ndvds6  12462  flodddiv4  12463  m1bits  12487  algrp1  12584  3lcm2e6woprm  12624  nn0gcdsq  12738  phiprmpw  12760  prmdiv  12773  prmdiveq  12774  pythagtriplem1  12804  pythagtriplem12  12814  pythagtriplem14  12816  pockthi  12897  infpnlem1  12898  4sqlem12  12941  4sqlem13m  12942  4sqlem19  12948  dec5dvds  12951  dec5nprm  12953  dec2nprm  12954  modxai  12955  modxp1i  12957  modsubi  12958  gcdmodi  12960  decsplit0b  12965  decsplit1  12967  decsplit  12968  karatsuba  12969  2exp7  12973  2exp8  12974  3exp3  12977  pwsbas  13341  subsubm  13532  mulg2  13684  subsubg  13750  unitsubm  14099  subsubrng  14194  subsubrg  14225  lsslss  14361  expghmap  14587  cnmpt1res  14986  rerestcntop  15248  rerest  15250  dvfvalap  15371  dvcnp2cntop  15389  dveflem  15416  plyun0  15426  dvply1  15455  reeff1oleme  15462  sin0pilem1  15471  sinhalfpilem  15481  cospi  15490  eulerid  15492  cos2pi  15494  ef2kpi  15496  sinhalfpip  15510  sinhalfpim  15511  coshalfpip  15512  coshalfpim  15513  sincosq3sgn  15518  sincosq4sgn  15519  cosq23lt0  15523  tangtx  15528  sincos4thpi  15530  sincos6thpi  15532  cosq34lt1  15540  rplogb1  15638  2logb9irr  15661  sqrt2cxp2logb9e3  15665  2logb9irrap  15667  binom4  15669  lgsdir2lem1  15723  lgsdir2lem2  15724  lgsdir2lem4  15726  lgsdir2lem5  15727  lgsne0  15733  1lgs  15738  gausslemma2dlem0e  15748  gausslemma2dlem0f  15749  gausslemma2dlem3  15758  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  lgsquad2lem2  15777  m1lgs  15780  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgsoddprmlem3a  15802  2lgsoddprmlem3b  15803  2lgsoddprmlem3c  15804  2lgsoddprmlem3d  15805  ex-fl  16172  ex-exp  16174  ex-bc  16176  012of  16444  2o01f  16445  qdencn  16483  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508