Theorem oveq1i 6017

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq1 6014	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

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  11277  imre  11377  crim  11384  remullem  11397  resqrexlemfp1  11535  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemnm  11544  absexpzap  11606  absimle  11610  amgm2  11644  maxabslemlub  11733  fsumconst  11980  modfsummod  11984  binomlem  12009  binom11  12012  arisum  12024  arisum2  12025  georeclim  12039  geo2sum  12040  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodfrecap  12072  fprodm1s  12127  fprodp1s  12128  fprodrec  12155  fprodmodd  12167  efzval  12209  resinval  12241  recosval  12242  efi4p  12243  tan0  12257  efival  12258  cosadd  12263  cos2tsin  12277  ef01bndlem  12282  cos1bnd  12285  cos2bnd  12286  absefib  12297  efieq1re  12298  demoivreALT  12300  eirraplem  12303  3dvds  12390  3dvdsdec  12391  3dvds2dec  12392  odd2np1  12399  nn0o1gt2  12431  nn0o  12433  5ndvds3  12460  5ndvds6  12461  flodddiv4  12462  m1bits  12486  algrp1  12583  3lcm2e6woprm  12623  nn0gcdsq  12737  phiprmpw  12759  prmdiv  12772  prmdiveq  12773  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem14  12815  pockthi  12896  infpnlem1  12897  4sqlem12  12940  4sqlem13m  12941  4sqlem19  12947  dec5dvds  12950  dec5nprm  12952  dec2nprm  12953  modxai  12954  modxp1i  12956  modsubi  12957  gcdmodi  12959  decsplit0b  12964  decsplit1  12966  decsplit  12967  karatsuba  12968  2exp7  12972  2exp8  12973  3exp3  12976  pwsbas  13340  subsubm  13531  mulg2  13683  subsubg  13749  unitsubm  14098  subsubrng  14193  subsubrg  14224  lsslss  14360  expghmap  14586  cnmpt1res  14985  rerestcntop  15247  rerest  15249  dvfvalap  15370  dvcnp2cntop  15388  dveflem  15415  plyun0  15425  dvply1  15454  reeff1oleme  15461  sin0pilem1  15470  sinhalfpilem  15480  cospi  15489  eulerid  15491  cos2pi  15493  ef2kpi  15495  sinhalfpip  15509  sinhalfpim  15510  coshalfpip  15511  coshalfpim  15512  sincosq3sgn  15517  sincosq4sgn  15518  cosq23lt0  15522  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  cosq34lt1  15539  rplogb1  15637  2logb9irr  15660  sqrt2cxp2logb9e3  15664  2logb9irrap  15666  binom4  15668  lgsdir2lem1  15722  lgsdir2lem2  15723  lgsdir2lem4  15725  lgsdir2lem5  15726  lgsne0  15732  1lgs  15737  gausslemma2dlem0e  15747  gausslemma2dlem0f  15748  gausslemma2dlem3  15757  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  lgsquad2lem2  15776  m1lgs  15779  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem3a  15801  2lgsoddprmlem3b  15802  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  ex-fl  16144  ex-exp  16146  ex-bc  16148  012of  16416  2o01f  16417  qdencn  16455  isomninnlem  16458  iswomninnlem  16477  ismkvnnlem  16480