Theorem oveq1i 6095

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  caov12  6278  map1  7101  exmidpw2en  7219  halfnqq  7777  prarloclem5  7867  m1m1sr  8128  caucvgsrlemfv  8158  caucvgsr  8169  pitonnlem1  8212  axi2m1  8242  axcnre  8248  axcaucvg  8267  mvrraddi  8543  mvlladdi  8544  negsubdi  8582  mul02  8714  mulneg1  8722  mulreim  8932  recextlem1  8979  recdivap  9048  2p2e4  9431  2times  9432  3p2e5  9446  3p3e6  9447  4p2e6  9448  4p3e7  9449  4p4e8  9450  5p2e7  9451  5p3e8  9452  5p4e9  9453  6p2e8  9454  6p3e9  9455  7p2e9  9456  1mhlfehlf  9523  8th4div3  9524  halfpm6th  9525  nneoor  9748  9p1e10  9779  dfdec10  9780  num0h  9788  numsuc  9790  dec10p  9819  numma  9820  nummac  9821  numma2c  9822  numadd  9823  numaddc  9824  nummul2c  9826  decaddci  9837  decsubi  9839  decmul1  9840  5p5e10  9847  6p4e10  9848  7p3e10  9851  8p2e10  9856  decbin0  9916  decbin2  9917  elfzp1b  10504  elfzm1b  10505  fz01or  10518  fz1ssfz0  10524  fz0to4untppr  10531  qbtwnrelemcalc  10690  fldiv4p1lem1div2  10740  1tonninf  10878  mulexpzap  11016  expaddzap  11020  sq4e2t8  11074  cu2  11075  i3  11078  iexpcyc  11081  binom2i  11085  binom3  11094  3dec  11152  faclbnd  11179  bcm1k  11198  bcp1nk  11200  bcpasc  11204  hashp1i  11251  hashxp  11267  hashpwfi  11269  hashfibc  11283  ccatlid  11374  pfxccatin12lem2c  11502  imre  11616  crim  11623  remullem  11636  sq01  11660  resqrexlemfp1  11775  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemnm  11784  absexpzap  11846  absimle  11850  amgm2  11884  maxabslemlub  11973  fsumconst  12221  modfsummod  12225  binomlem  12250  binom11  12253  arisum  12265  arisum2  12266  georeclim  12280  geo2sum  12281  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodfrecap  12313  fprodm1s  12368  fprodp1s  12369  fprodrec  12396  fprodmodd  12408  efzval  12450  resinval  12482  recosval  12483  efi4p  12484  tan0  12498  efival  12499  cosadd  12504  cos2tsin  12518  ef01bndlem  12523  cos1bnd  12526  cos2bnd  12527  absefib  12538  efieq1re  12539  demoivreALT  12541  eirraplem  12544  3dvds  12631  3dvdsdec  12632  3dvds2dec  12633  odd2np1  12640  nn0o1gt2  12672  nn0o  12674  5ndvds3  12701  5ndvds6  12702  flodddiv4  12703  m1bits  12727  algrp1  12824  3lcm2e6woprm  12864  nn0gcdsq  12978  phiprmpw  13000  prmdiv  13013  prmdiveq  13014  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem14  13056  pockthi  13137  infpnlem1  13138  4sqlem12  13181  4sqlem13m  13182  4sqlem19  13188  dec5dvds  13191  dec5nprm  13193  dec2nprm  13194  modxai  13195  modxp1i  13197  modsubi  13198  gcdmodi  13200  decsplit0b  13205  decsplit1  13207  decsplit  13208  karatsuba  13209  2exp7  13213  2exp8  13214  3exp3  13217  ballotfilem1  13220  ballotfilem2  13228  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemfrceq  13272  ballotfilemth  13281  subsubm  13790  mulg2  13934  subsubg  14000  gsumconstcmn  14166  pwsbas  14205  unitsubm  14426  subsubrng  14522  subsubrg  14553  lsslss  14718  expghmap  14942  cnmpt1res  15397  rerestcntop  15659  rerest  15661  dvfvalap  15782  dvcnp2cntop  15800  dveflem  15827  plyun0  15837  dvply1  15866  reeff1oleme  15873  sin0pilem1  15882  sinhalfpilem  15892  cospi  15901  eulerid  15903  cos2pi  15905  ef2kpi  15907  sinhalfpip  15921  sinhalfpim  15922  coshalfpip  15923  coshalfpim  15924  sincosq3sgn  15929  sincosq4sgn  15930  cosq23lt0  15934  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  cosq34lt1  15951  logfac  15995  rplogb1  16050  2logb9irr  16073  sqrt2cxp2logb9e3  16077  2logb9irrap  16079  binom4  16081  log2tlbndlog2  16082  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  lgsdir2lem1  16147  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsne0  16157  1lgs  16162  gausslemma2dlem0e  16172  gausslemma2dlem0f  16173  gausslemma2dlem3  16182  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  lgsquad2lem2  16201  m1lgs  16204  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgsoddprmlem3a  16226  2lgsoddprmlem3b  16227  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  ex-fl  16739  ex-exp  16741  ex-bc  16743  depindlem1  16747  012of  17023  2o01f  17024  qdencn  17072  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102