Theorem oveq1i 6027

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 6024	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Syntax hints:   = wceq 1397  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  caov12  6210  map1  6986  exmidpw2en  7103  halfnqq  7629  prarloclem5  7719  m1m1sr  7980  caucvgsrlemfv  8010  caucvgsr  8021  pitonnlem1  8064  axi2m1  8094  axcnre  8100  axcaucvg  8119  mvrraddi  8395  mvlladdi  8396  negsubdi  8434  mul02  8565  mulneg1  8573  mulreim  8783  recextlem1  8830  recdivap  8897  2p2e4  9269  2times  9270  3p2e5  9284  3p3e6  9285  4p2e6  9286  4p3e7  9287  4p4e8  9288  5p2e7  9289  5p3e8  9290  5p4e9  9291  6p2e8  9292  6p3e9  9293  7p2e9  9294  1mhlfehlf  9361  8th4div3  9362  halfpm6th  9363  nneoor  9581  9p1e10  9612  dfdec10  9613  num0h  9621  numsuc  9623  dec10p  9652  numma  9653  nummac  9654  numma2c  9655  numadd  9656  numaddc  9657  nummul2c  9659  decaddci  9670  decsubi  9672  decmul1  9673  5p5e10  9680  6p4e10  9681  7p3e10  9684  8p2e10  9689  decbin0  9749  decbin2  9750  elfzp1b  10331  elfzm1b  10332  fz01or  10345  fz1ssfz0  10351  fz0to4untppr  10358  qbtwnrelemcalc  10514  fldiv4p1lem1div2  10564  1tonninf  10702  mulexpzap  10840  expaddzap  10844  sq4e2t8  10898  cu2  10899  i3  10902  iexpcyc  10905  binom2i  10909  binom3  10918  3dec  10975  faclbnd  11002  bcm1k  11021  bcp1nk  11023  bcpasc  11027  hashp1i  11073  hashxp  11089  ccatlid  11182  pfxccatin12lem2c  11310  imre  11411  crim  11418  remullem  11431  resqrexlemfp1  11569  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemnm  11578  absexpzap  11640  absimle  11644  amgm2  11678  maxabslemlub  11767  fsumconst  12014  modfsummod  12018  binomlem  12043  binom11  12046  arisum  12058  arisum2  12059  georeclim  12073  geo2sum  12074  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodfrecap  12106  fprodm1s  12161  fprodp1s  12162  fprodrec  12189  fprodmodd  12201  efzval  12243  resinval  12275  recosval  12276  efi4p  12277  tan0  12291  efival  12292  cosadd  12297  cos2tsin  12311  ef01bndlem  12316  cos1bnd  12319  cos2bnd  12320  absefib  12331  efieq1re  12332  demoivreALT  12334  eirraplem  12337  3dvds  12424  3dvdsdec  12425  3dvds2dec  12426  odd2np1  12433  nn0o1gt2  12465  nn0o  12467  5ndvds3  12494  5ndvds6  12495  flodddiv4  12496  m1bits  12520  algrp1  12617  3lcm2e6woprm  12657  nn0gcdsq  12771  phiprmpw  12793  prmdiv  12806  prmdiveq  12807  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem14  12849  pockthi  12930  infpnlem1  12931  4sqlem12  12974  4sqlem13m  12975  4sqlem19  12981  dec5dvds  12984  dec5nprm  12986  dec2nprm  12987  modxai  12988  modxp1i  12990  modsubi  12991  gcdmodi  12993  decsplit0b  12998  decsplit1  13000  decsplit  13001  karatsuba  13002  2exp7  13006  2exp8  13007  3exp3  13010  pwsbas  13374  subsubm  13565  mulg2  13717  subsubg  13783  unitsubm  14132  subsubrng  14227  subsubrg  14258  lsslss  14394  expghmap  14620  cnmpt1res  15019  rerestcntop  15281  rerest  15283  dvfvalap  15404  dvcnp2cntop  15422  dveflem  15449  plyun0  15459  dvply1  15488  reeff1oleme  15495  sin0pilem1  15504  sinhalfpilem  15514  cospi  15523  eulerid  15525  cos2pi  15527  ef2kpi  15529  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  sincosq3sgn  15551  sincosq4sgn  15552  cosq23lt0  15556  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  cosq34lt1  15573  rplogb1  15671  2logb9irr  15694  sqrt2cxp2logb9e3  15698  2logb9irrap  15700  binom4  15702  lgsdir2lem1  15756  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsne0  15766  1lgs  15771  gausslemma2dlem0e  15781  gausslemma2dlem0f  15782  gausslemma2dlem3  15791  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  lgsquad2lem2  15810  m1lgs  15813  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgsoddprmlem3a  15835  2lgsoddprmlem3b  15836  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  ex-fl  16321  ex-exp  16323  ex-bc  16325  012of  16592  2o01f  16593  qdencn  16631  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656